Dyvercon
Kry10, in collaboration with Proofcraft, aims to enable a new class of embedded and cyber-physical systems, with formally assured support for updatable multicore systems built on the verified seL4 microkernel. For multicore, Dyvercon will use a multikernel configuration of seL4, with a separate seL4 kernel instance per core. For zero-downtime software and configuration updates, they will develop a privileged user-space component that provides a high-level API for authenticating and executing update commands. For formal assurance, they will develop theorem-proving frameworks for verifying kernel-level correctness of multikernel configurations and user-level correctness of privileged components. A major verification challenge is concurrency amongst multiple kernel instances and user-space threads.
The project members are:
- Kry10
- Proofcraft
Contributions to formal verification
Demonstration system
As a demonstration, Kry10 will develop a mechatronics teaching system. The system will package a small robotic device with a series of exercises teaching control theory and secure system development. Students will complete exercises by issuing software updates to the system, using multiple cores to distribute processes. The system will demonstrate a security property, that students will not be able to gain full control of the system, even though they can deploy code to parts of it.
Verified parts of the system
- The seL4 microkernel, already verified for single-core configurations, with substantial progress towards verification for multikernel configurations.
- Privileged user-space components responsible for system configuration and zero-downtime updates.
- Parts of peripheral device drivers responsible for configuring Direct Memory Access (DMA).
- A system integrity property, that unverified components cannot break invariants enforced by verified components.
To reach its goal, Kry10 and Proofcraft will develop
- Kernel-level verification frameworks, for reasoning about concurrent systems, focusing on maximising reuse of existing sequential verification.
- User-space verification frameworks, for specifying and verifying functional safety and integrity of concurrent dynamic seL4-based system designs, focusing on compositionality and proof automation.
- A systematic approach to high-assurance dynamic system design, with support for incremental updates, and tools to help developers specify and build secure-by-design dynamic systems.
- A multikernel configuration of seL4, allowing the use of multiple CPU cores, with formal assurance that will be increase over the course of the project, and can later be extended to full symmetric multiprocessing (SMP).
- A method for ensuring the safe configuration of peripheral devices that use legacy Direct Memory Access (DMA), to protect system integrity in the presence of untrusted devices drivers.
- A reference platform, including a software development kit and a supported hardware configuration, that encapsulates the results of the project.
Matt Brecknell
E-Mail: matt[at]kry10[dot]com