Automatic Derivation of Kernel Locks for OpenBSD

  • Supervisor Dr. Joseph Kiniry
  • Subject Area Software Engineering
  • Pre-requisites Very good knowledge of C
  • Co-requisites (things you must learn along the way) Good knowledge of UNIX (generally) and OpenBSD (specifically), concurrency and threads, constraint anlysis, program specification, static program checking, and OS-level systems programming
  • Subject Coverage Programming Languages, Compilers, Concurrency, Static Analysis
  • Project Type Design and Implementation
  • Hardware Any computer running OpenBSD

Description

OpenBSD is widely regarded as the world's most secure operating system. It represents the combined effort of hundreds of dedicated individuals, most of whom work in their spare time for free, over nearly a decade.

OpenBSD developers try very hard to write code that is well-designed, clean, maintainable, but above all, secure. A number of techniques are used for such, but most of them are relatively ad hoc when compared to the kind of program development that that KindSoftware research group regularly participates in.

Multi-processor/-core support is a relatively recent addition to OpenBSD. Given OpenBSD's focus on correctness above all else, a fairly simple single-lock-based design was used, similar to that adopted by other FLOSS UNIXen, to implement this new feature.

Unfortunately, while such and implementation is simple, it does not exhibit high performance, it is difficult to maintain and reason about, and can easily exhibit unnecessary deadlock.

The goal of this project is to investigate the possibility of adding atomicity specifications to the OpenBSD kernel in such a way as to automatically generate minimal correct lock covers for kernel code.

Mandatory Goals

  1. Gain familiarity with OpenBSD.
  2. Gain familiarity with SMT support in OpenBSD.
  3. Gain familiarity with reasoning frameworks for concurrency and atomicity.
  4. Design and develop SMT support in OpenBSD, including concurrency and atomicity annotations, lock specifications, etc.
  5. Coauthor, submit, and publish a paper on this work.

Discretionary Goals

  1. Design and develop a lock cover static analysis tool to determine minimal lock sets and covers for correct, high-performance kernel locks.
  2. Release the framework and tools to the world under an appropriate FLOSS license, hopefully so that it will be incorporated into, and used by, OpenBSD.

Sources of Information and Preparatory Reading

  1. OpenBSD
  2. SMT in OpenBSD
  3. See the following OpenBSD source files:
    • src/sys/sys/kern_lock.c
    • src/sys/sys/mplock.c
    • src/sys/sys/lock.h
    • src/sys/kern/sched_bsd.c
    • src/sys/kern/mplock.c
    • src/sys/kern/mplock.c