CSP Final Project - Formal verification

In the final project, you are required to choose an aspect of operating system that you are interested in and build a model of this aspect. You should also describe several verification efforts that represents the state of art on this aspect. Suggested aspects include memory management, process management, IPC, scheduling, file system, network, etc. Or you can choose trending hardware features like RDMA, NVM, SGX etc. You are suggested to focus on a specific aspect rather than looking at the whole operating system. However, the aspect should have some complexity, rather than a simple data structure implementation (e.g., linked lists, stacks and queues). Here are some more suggestions for writing the paper.

• Basic verification target: functionality. Describe a concrete prototype implementation in your mind. A sequential implementation is enough (concurrency is welcome but much harder).The primary goal is to fulfill the functionality (you can sacrifice some performance if it makes your system easier to reason about). What data structures are necessary to implement the functionality? How would you model your system, i.e., abstract the implementation to hide the implementation details? The model would be your specification, or the interfaces to be used by others.
• Other features or properties. A file system would require crash-safety. Operating system would want non-inteference. What features are most important and desired to be verified for your system? Or you could just summarize some properties or invariants of your system. E.g., a file system should be a tree shape. Or the page table root must be exclusively owned by a single process.
• State of the art. Which previous efforts have tried to verify this aspect? How do they make specifications and what properties do they verify? What new techniques do they propose to verify the system? You can compare these efforts and show their pros and cons.
• Focus on specification. As we didn’t systematically teach you how to make proofs. So no proof efforts are required. But you should understand your system and try to specify your system. The specification includes the abstract state that represents the logical layout of the concrete data structure and the abstract operations that correspond to concrete operations.

Papers for reference:

• [SOSP’17] Hyperkernel: push-button verification of an OS kernel
• [OSDI’18] Nickel: a framework for design and verification of information flow control systems
• [SOSP’17] Verifying a high-performance crash-safe file system using a tree specification
• [SOSP’19] Verifying software network functions with no verification expertise
• [OSDI’16] CertiKOS: an extensible architecture for building certified concurrent OS kernels
• [OSDI’18] Verifying concurrent software using movers in CSPEC
• [SOSP’19] Using Concurrent Relational Logic with Helpers for verifying the AtomFS file system
• More papers can be found in the following courses
  • [OSDI'20] Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel
  • [OSDI'20] Cobra: Making Transactional Key-Value Stores Verifiably Serializable
  • [OSDI'20] Determinizing Crash Behavior with a Verified Snapshot-Consistent Flash Translation Layer
  • [OSDI'20] Storage Systems are Distributed Systems (So Verify Them That Way!)
  • https://6826.csail.mit.edu/2019/schedule.html
  • http://read.seas.harvard.edu/~kohler/class/cs260r-17/
  • https://courses.cs.washington.edu/courses/cse599w/16sp/
• More related the papers you find, more scores you would get :)