Tutorial on Formal Verification of Security Protocols (Canceled)

2pm~6pm on Tuesday, October 9


The goal of this tutorial is to discuss the correct design of secure protocols, common kinds of attacks on protocols and how to detect and stop these attacks. Formal methods for verifying protocols such as deductive-reasoning and model checking are presented and the tools that can be used to automate the formal analysis of protocols are introduced. This tutorial focuses in particular on an automated logic-based technique (deductive-reasoning method) developed by Dr. Anca Jurcut et al. at the University of Limerick and at the University College Dublin in Ireland.

Workshop on Formal Methods and Software Verification

9~12am on Saturday, October 13

 This workshop aims at in-depth discussions among researchers and practitioners working on formal methods and software verification in South Korea. Three work-in-progress topics will be presented and discussed among participants, such as  machine learning and false-alarm filtering, model checking block-chains, and automotive safety in practice. Anybody interested is welcome, but the working language is Korean.

Presentation 1 : Prof. Shin Hong
(Handong Global University, South Korea)

Protecting Static Analysis False Positives by Learning from Alarm Review Data

Static analysis in Continuous Integration can significantly improve the quality of a Software Under Development, because it enables early detection of defects in a fully automated way. However, static analysis also produces a large number of false positive alarms whose identification/elimination takes up valuable developer time, and hinder their applications in practice.

This talk presents our work-in-progress on an automated classifier based on Convolutional Neural Networks (CNNs). Our hypothesis is that many of false positives can be classified as such by identifying specific lexical patterns in the parts of code that raised the alarm. In the talk, we will present our current approach to train a CNN based classifier to learn and detect these lexical patterns, using a total of about 10K historical static analysis alarms generated by six static analysis checkers their labels assigned by actual developers.  The pilot study results indicate that our approach can be highly effective for identifying false positive alarms.

Presentation 2 : Prof. Eun-Kyung Ji
(KAIST, South Korea)

Modeling and Verification of a Blockchain Consensus Protocol

A blockchain is a type of distributed ledger that can record transactions between parties in a verifiable and permanent way. Each node has its own ledger, and the contents of each ledger are kept the same by the consensus algorithm. It is essential to ensure safety and fault tolerance of the consensus algorithms in blockchain platforms. The Stellar Consensus Protocol (SCP) is a construction for federated Byzantine agreement. With the purpose of investigation and evaluation of the SCP, we modeled it as timed automata and verified the SCP model in several aspects such as correctness, fault tolerance, and open membership by using simulation and model checking techniques. This talk presents how we conducted modeling and verification of the SCP and what we have learned. The analysis results of the SCP and discussion topics are also be presented.

Presentation 3 : Jun-Yeol Choi
Mando, South Korea)

자동차 시스템 검증의 현재와 미래

자동차 산업은 ISO-26262, A-SPICE 표준의 제정과 함께 검증활동의 중요성이 기존대비 강조되었습니다. 현재 현업에서는 표준에따라 검증활동을 진행하고 있으나, 차량에서의 문제점들은 지속적으로 발견되고 있습니다. 결국 급변하는 자동차 산업에서 검증활동 역시 발빠르게 개선 되어야하는 상황입니다. 브레이크 도메인에서 현재 사용 중인 검증활동들을 소개하고, 현업에서 느끼는 검증활동의 한계와 앞으로의 방향에 대해 설명합니다.