Projects

Grant

Research Interest

Software Formal Verification (정형 검증)

We are working with multiple methods to build software security and reliability, such as fuzzing, program synthesis, and so on. However, one of the strongest ways that we are using to fully guarantee software assurance is "formal verification". In this sense, several our projects are related to formal verification, "the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics (from Wikipedia)". Formal verification requires multiple components 1) a target program, 2) a mathematical specification for the program, 3) a mathematical relation to define the consistency between the program and the specification, and proofs and a proof checker to actually show the correctness of the program and the specification. The below figure shows how key components in formal verification are related to others.

Formal verification has several granularities, and (as mentioned) it is the most strongest way to guarantee the correctness of the software (by showing the target software faithfully implements the rigorous specification). However, it is not practical due to the high verification cost. My main works are related to reducing the cost while fully facilitating the power of formal verification. To do that, we usually use modular way to separately verify multiple components in the software and compose those proofs together to show the entire correctness as the below figure shows.

We and our collaborators are working on formal verifications (and other methodologies which are mentioned above - e.g., fuzzing, program synthesis) for the following targets. 

Machine Learning Models (머신 러닝 모델)

The Software 2.0 era has seen a significant increase in neural network-based software and services, raising concerns about potential costs related to neural network failures. Formal verification stands out as the singular approach to ultimately guarantee correctness, but challenges persist in the application of formal verification to this domain. Even state-of-the-art techniques for neural network verification face limitations in two crucial verification components. Current methodologies do not fully illustrate the complete behavior of neural networks as formal specifications; instead, these techniques primarily focus on local robustness. Furthermore, they continue to struggle with the efficient management of large-scale models and face challenges in achieving optimal reusability. 

To address the stated challenges, our objective is to develop the foundational theory and methodology for neural network verification. Drawing inspiration from concepts in the formal verification of conventional software and considering the distinctive characteristics of neural network domains, we aim to create a methodology that precisely articulates multiple desired properties of target networks in a mathematically rigorous manner, without restricting the types of these properties. Furthermore, we put forward a modular verification approach based on both the stated specifications and the target network structure. We are confident that our endeavors will boost the reliability of neural networks, thereby opening pathways for building critical network-related applications and societal advancements.

Distributed Systems and Blockchain (분산 시스템 및 블록체인)

A distributed service platform is a set of components unified by a management control plane that implements standard network services. Building a distributed service platform usually requires multiple local machines, a network to connect those local machines to others, distributed systems to provide the unified abstractions of those multiple local machines, and the application that we hope to provide for users. 

The low-level parts of distributed systems are usually built with distributed consensus protocols that guarantees the consistency in a certain level. Among them, there are several strongly consistent protocols such as Paxos, Raft, and Chain-replication. They provides the strong guarantee that users view the same state regardless of any kinds of network and local machine errors in distributed systems. However, due to the complexity of those protocols, application builders usually use State Machine Replication (SMR) as a abstraction of those protocols that are used for the same purpose. However, SMR sacrifices possessing all possible behaviors (i.e., partial failures) of those protocols in the model. Therefore, we work on providing a proper but simple program abstraction for multiple distributed protocols and systems with formal verification.

Also, We provide template-driven protocol safety proof (linearizability) for developers to enable them not to consider distributed features while writing specifications and programs in their development. 

This work also can be extended to multiple areas, especially for blockchain protocols and other distributed protocols and systems (e.g., weekly consistent protocols and systems).

Operating Systems and Hypervisor (운영체제 및 가상화 머신)

Operating systems and hypervisors are backbones of local machines. Furthermore, they are the backbone of any kind of software. We and our collaborators are building tools and security guarantee proofs for real world operating system and hypervisor codes. 

Our main targets are 1) small key concurrent modules in Linux and 2) security critical parts of protected KVM, which will be the security base of the android ecosystem in the near future.

Machine Learning Platforms (머신 러닝 플랫폼)

People are using machine learning platforms to build and train their one machine learning models. Two most famous platforms are TensorFlow and PyTorch. We are working on developing tools for better analysis (including debugging) when using those platforms. We especially focus on TensorFlow.

Smart Contracts (스마트 컨트랙트)

A smart contract is "a self-executing contract with the terms of the agreement between buyer and seller being directly written into lines of code (from Wikipedia)". Definitely, it is extremely sensitive to bugs and bleaches. Therefore, we are building the tool to improve the correctness guarantee for a smart contract. 

A smart contract also usually requires checks from non-exports on programming. They should be exports on contract domains but may not have enough knowledge to check the programmed contracts. To resolve this, we work on smart contact synthesis.