Welcome to Jieung Kim's Page
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
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.© Jieung Kim. All Rights Reserved. Designed by HTML Codex