Pancake is a new language with a verified compiler and an automated Viper front-end; it is used to verify a performant Ethernet NIC driver, though the transpiler and reentry semantics remain unverified.
Fast, Secure, Adaptable: LionsOS Design, Implementation and Performance
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
abstract
We present LionsOS, an operating system for security- and safety-critical embedded systems. LionsOS is based on the formally verified seL4 microkernel and designed with verification in mind. It uses a static architecture and features a highly modular design driven by strict separa- tion of concerns and a focus on simplicity. We demonstrate that LionsOS achieves excellent performance on system-call intensive workloads.
fields
cs.PL 1years
2025 1verdicts
CONDITIONAL 1representative citing papers
citing papers explorer
-
Verifying Device Drivers with Pancake
Pancake is a new language with a verified compiler and an automated Viper front-end; it is used to verify a performant Ethernet NIC driver, though the transpiler and reentry semantics remain unverified.