Formal Verification Made Easy (and fast!)
Talkat Open Source Summit Europe + Embedded Linux Conference Europe 2019 · on Wednesday, 2019-10-30· at 16:15· Forum 2·
summary
Modeling PREEMPT_RT as synchronised automata produces a runnable verifier that moves from offline traces to an in-kernel checker translated from the formal model to C by a Python generator. The end-to-end model reaches 9000 states and 23,000 transitions, uses about 8 KB for the big model, turns 30 s of fine-grained traces into 2.5 GB of data if fully traced, and found four bugs that other Linux tools miss. Online verification runs via tracepoints with lower overhead than full tracing and is practical for production use.
AI-written summary · about
chapters (11)
- 0:00Introduction to speaker
- 0:35Challenges in Linux safety
- 3:51Applying formal methods
- 4:57Automata and synchronization
- 10:30Modeling complex behavior
- 16:05Runtime verification process
- 18:38Implementing C code
- 22:49Performance analysis
- 24:38Benchmarks and results
- 27:33Future work and conclusion
- 31:34Q&A
related talks
46mA Maintainable, Scalable, and Verifiable SW Qualification Approach for Automotive in Linux
24mDemocratising Formal Verification of RISC V Processors
01h 33mRISC V Verification for Processor Cores and Optional Custom Extensions
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
38mAlice in Kernel Land: Lessons Learned From the eBPF Rabbit Hole
06mFormal Verification with the Certora Prover
33mApplicable and Achievable Formal Verification
17mVEP: A Two-stage Verification Toolchain for Full eBPF Programmability