Home

Project ideas

• Add an optimization to CompCert
• Add features to a proven-correct OS
  • seL4
  • Verve
• Prove systems optimizations correct, in a real system or in a model of a system
  • I/O buffering (that stdio is “correct”)
  • Prefetching in a networked file system
  • Web cache policy correctness
  • Click Classifier optimization https://github.com/kohler/click/blob/master/elements/standard/classification.cc
• Prove correctness of a system using speculation
  • System proceeds based on an assumption, only commits results when assumption is verified
  • Example: Speculator https://www.cs.cmu.edu/~dga/15-849/papers/speculator-sosp2005.pdf
  • Example: xsyncfs https://www.usenix.org/legacy/event/osdi06/tech/nightingale/nightingale.pdf
• Prove information flow facts about data-backed systems
  • Many examples in HotCRP
  • Information about each paper is restricted to certain classes of user
  • Example: Decision (yes/no) is visible to (1) authors + all PC members, or (2) all PC members, or (3) only non-conflicted PC members, depending on settings
  • But any user can search for papers with particular decisions: decision:yes or NOT decision:no
  • Search should return just visible results; requires that policy be applied at the right places
  • Advanced: Support database optimization—select paperId from Paper where decision>0 for decision:yes is safe, select paperId from Paper where not (decision<0) for NOT decision:no is not safe
• Prove facts about commit protocols in an in-memory database
  • Optimistic concurrency control
  • Read/write locking