Grant

Research Interest

Formal Verification Projects

Most of my 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 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.

Machine Learning Model Correctness Verification

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.

ADO: Atomic Distributed Objects - Distributed System Verification

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 (See the below figure).

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.

Formal verification on pKVM

pKVM is a hypervisor for Android to increase security in the future Android ecosystem. Please look at the below video to learn more about pKVM.


We are developing end-to-end formal verification tools for pKVM and verify it! It includes the following things.

• A language for writing formal specifications and tests for specifications.
• Novel composition theory and tool for formal verification.
• Automated tools to reduce the human cost in the formal verification.
• Formally defined hardware specifications.
• Translation validations for the C code compilation.

CertiKOS

CertiKOS is an extensible architecture for building certified concurrent OS kernels. Complete formal verification of a non-trivial concurrent OS kernel is widely considered a grand challenge. We present a novel compositional approach for building certified concurrent OS kernels. CertiKOS is not a fully practical operating system, but contains multiple services that can be used with restricted purposes. The below figure shows how we build CertiKOS with 6500 lines of C and x86 assembly.

With the kernel, the main purpose of our formal verification is showing that all user programs running on top of our formal specification faithfully reflects the all behaviors of running the same user programs on top of the kernel implementation (see below).

To show that, we aggressively decompose the kernel into multiple layers (65 layers) and granulary provide abstractions of each layer. The below figure shows the overall module hierarchy of CertiKOS.

Each model contains multiple layers in it to ease the verification process. For example, MCS Lock formal verification consists of six layers to provide the abstracted lock specification that can also be used as a specification of other lock algorithms and implementations (e.g., ticket lock).

We are working on improving the methodologies that we have used in CertiKOS and extending CertiKOS. Possible extensions are as follows.

• CertiKOS ARM Hypervisor: verifying functional correctness and security property (integrity and confidentiality of CertiKOS hypervisor on ARM platform
• Concurrent Linking Framework: providing a user-friendly framework to link multiple separate instances in concurrent program verification and link CeriKOS proofs using this framework as an example
• User Program Linking: providing a framework to link separately developed and verified user programs with CertiKOS

Other Projects

Quantization Benchmarks

Quantization is the process of mapping continuous infinite values to a smaller set of discrete finite values and it is one of the most prevelent optimization techniques for machine learning models. We are working on how to measure the effect of multiple quantization options.

Smart Contract Synthesis

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. We are working on building a tool to automatically synthesize smart contracts for specific domains.