Verified Abstract Machines for Operating Systems – VeriAMOS

General-purpose Operating Systems (OSes), such as Linux, are
increasingly used in the safety-critical embedded systems industry,
with usage in automotive, medical and cyber-physical systems.
However, it is well known that general purpose OSes suffer from bugs.
Recently, some major advances have been made in verifying OS kernels,
mostly employing interactive theorem-proving techniques.
Nevertheless, these approaches incur the cost of a huge user-assisted
proving effort, not only during the design, implementation and proving
phases but also when maintaining the OSes or extending them with new
features. Therefore, scaling such techniques to verify all OS
services remains a challenge.

An alternative that has not previously investigated in the context of
OS services is the use of automated static analysis. Automated static
analysis tools compute program invariants and semantic properties,
without human intervention. These tools rely on abstractions that
describe a range of program invariants and properties, and on
algorithms to compute invariants that hold true for all program
executions. Still, while sound, static analyzers are incomplete,
meaning that they may fail to prove a valid program correct, instead
conservatively reporting it as "possibly incorrect". The complex data
structures, low level operations, and concurrency intrinsic to OS code
further raise the difficulty of applying automated static analysis
tools in an OS setting.

The VeriAMOS project brings together experts in static analysis,
operating systems, and programming language design, at Inria, Sorbonne
University, and the University of Grenoble, to propose a new approach
to producing verified OS services, based on the use of Domain-Specific
Languages (DSLs) and automated static analysis. A DSL is a
programming language that is designed around abstractions that are
specific to a family of programs. A DSL lets programmers implement a
specific class of algorithms at a higher level than a conventional
programming language, and provides a compilation chain to produce
target code. By limiting the language expressiveness, a DSL also
constrains programmers, and prevents the misuse of language features.
The key insight behind the VeriAMOS project is that by raising the
level of abstraction and restricting the program design space, DSLs
can make it possible to fully automate strong verifications on
implementations of real OS services.

As a showcase for the proposed approach, the VeriAMOS project will
focus on I/O schedulers. Recent years have seen the introduction of a
number of new, complex I/O schedulers to meet the challenges raised by
SSDs, which provide much greater performance than traditional rotating
disks and are attractive in the context of embedded systems, due to
their shock resistance. VeriAMOS will target properties such as no
loss or corruption of requests and freedom from starvation, that are
critical in a SSD I/O scheduler implementation. Challenges include
the design, automation, and deployment of relevant abstractions to
support the static analysis and the definition of an expressive, high
level programming framework that ensures the generation of efficient
and provably correct scheduling policies. To overcome these
challenges, synergy is needed between the domains of static analysis,
operating systems, and programming language design to ensure that the
static analysis is able to reason about the chosen programming
constructs and the chosen programming constructs are sufficient to
implement real scheduling policies.

While the VeriAMOS project will focus on the domain of I/O schedulers,
we strongly believe that this work will pave the way towards the
automatic verification of other OS services. As a result, creating
fully verified critical services will no longer to be limited to a few
proof experts, but will be accessible to a wide spectrum of systems
code developers.