PISTIs-V addresses the lack of an integrated IT stack with provable end-to-end security for embedded/cyber-physical systems. It aims to develop a reference system with proofs of strong safety and security properties covering hardware and software and their interaction. Specifically, PISTIs-V will verify that the new LionsOS operating system (OS) operates to specification and enforces security and safety properties, including the prevention of unauthorised leaking of sensitive data and the guarantee of real-time deadlines, making use of formally verified hardware components. A core enabler of the work will be Pancake, a new systems programming language with a verified compiler.

The project members are:

• PlanV
• UNSW Sydney
• University of Gothenburg

Demonstration system

PISTIs-V will develop an FPGA-based reference system for cyber-physical systems on a partially-verified RISC-V processor that demonstrates strong security and safety guarantees, including absence of unauthorised information flow and guarantee of real-time deadlines in the presence of untrusted components. 

Verified parts of the IT system

• Critical hardware components, including the memory-management unit, a crypto accelerator, the fence.t instruction (required for preventing information leakage) and several device controllers (incl Ethernet);
• LionsOS device drivers for the verified device controllers;
• Other LionsOS components critical to controlling information flow;
• Extensions to the (previously verified) seL4 microkernel for preventing unauthorised information flow through micro-architectural state (caches etc).

Goals of PISTIs-V

• Enable the first-ever verification of controllers and drivers for real-world devices, such as Ethernet, by developing a formalism for specifying the software interface of device controllers;
• Develop the Pancake programming language to allow its use for implementing device drivers without the need for non-Pancake code, and verify that the binary code generated by the compiler retains the precise semantics of the Pancake program;
• Verify Verilog implementations of device controllers against the device interface specification;
• Formally connect correctness proofs (using interactive theorem proving in Isabelle/HOL or HOL4 or automated provers based on SMT solvers) of LionsOS components to the verified seL4 specification, resulting in the first end-to-end verification of user-mode components on a verified OS kernel;
• Prove that, with the help of the fence.t instruction, seL4 will be the first (and only) OS kernel that can prevent micro-architectural covert channels (this prevention will transfer to LionsOS);
• Develop a formalism for specifying system-wide security policies and verify that they are enforced by LionsOS, making LionsOS the first ever OS with verified end-to-end security enforcement;
• Perform a sound and complete worst-case execution time (WCET) analysis of seL4 on a RISC-V processor and develop a reasoning framework that utilises the results of this analysis to guarantee deadlines of critical real-time components, making LionsOS the first OS verified to guarantee timeliness of mixed-criticality systems.