Current Project

Formal verification on pKVM

  • pKVM is a hypervisor for Android
  • Develop an end-to-end formal verification tool for pKVM and verify it!

Previous Projects

ADVERT: Atomic Distributed System Verification Toolkit

  • Build a verification template for quorum-based distributed systems
  • Provide compositions of multiple distributed systems to form a bigger system
  • 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

CertiKOS

  • Present a novel compositional approach for building certified concurrent OS kernels and develop a practical concurrent OS kernel and verify its (contextual) functional correctness in Coq
    • It is written in 6500 lines of C and x86 assembly
    • It is the first proof of functional correctness of a complete, general-purpose concurrent OS kernel with fine-grained locking
    • It runs on stock x86 multicore machines
  • Work on extending CertiKOS in many ways:
    • 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

Publications

Thesis

Jieung Kim (Yale University), Modular and Compositional Development of Certified Concurrent Software Systems (Ph.D. Thesis)

Jieung Kim (KAIST), Proving FFMM Type Safety Using Coq (MS Thesis)

Journal

Ronghui Gu, Zhong Shao, Hao Chen, Jieung Kim, Jeremie Koenig, Xiongnan (Newman) Wu, Vilhelm Sjoberg, and David Costanzo, Building Certified Concurrent OS Kernels, Communications of the ACM, 62(10), pages 89-99, October 2019.

Conference

Wolf Honore*, Jieung Kim*, Ji-Yong Shin, and Zhong Shao , Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed Systems Proceedings of 2021 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'21), October 2021. (*: both equally contribute to this work)

Ji-Yong Shin, Jieung Kim, Wolf Honore, Hernan Vanzetto, Srihari Radhakrishnan, Mahesh Balakrishnan, and Zhong Shao , WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems, ACM Symposium on Cloud Computing 2019 (SoCC ’19), November 2019.

Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jeremie Koenig, Vilhelm Sjoberg, Hao Chen, David Costanzo, and Tahina Ramananandro, Certified Concurrent Abstraction Layers, Proceedings of 2018 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2018.

Jieung Kim, Vilhelm Sjoberg, Ronghui Gu, and Zhong Shao, Safety and Liveness of MCS Lock—Layer by Layer, Proceedings of the 15th Asian Symposium on Programming Languages and Systems, November 2017.

Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjoberg, and David Costanzo, CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels, 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16), November 2016.

Jieung Kim, Sukyoung Ryu, Victor Luchangco, and Guy L. Steele Jr., Fine-Grained Function Visibility for Multiple Dispatch with Multiple Inheritance, Proceedings of the 11th Asian Symposium on Programming Languages and Systems, December 2013.

Jieung Kim and Sukyoung Ryu, Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance, The First International Conference on Certified Programs and Proofs, December 2011.

Poster

Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jeremie Koenig, Vilhelm Sjoberg, Hao Chen, David Costanzo, and Tahina Ramananandro, Certified Concurrent Abstraction Layers, Proceedings of 2018 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2018.

Technical Report

Ji-Yong Shin, Jieung Kim, Wolf Honore, Hernan Vanzetto, Srihari Radhakrishnan, Mahesh Balakrishnan, and Zhong Shao, Write-Once-Registers: A Modular Foundation for Simple, Verifiable Distributed Systems, Technical report - YALEU/DCS/TR1544, December 2018

Jieung Kim and Sukyoung Ryu, Coq Mechanization of Featherweight Basic Core Fortress for Type Soundness, Technical Report (ROSAEC-2011-011), May 2011.


Talks & Lectures