The MemCAD static analyser: shape, value and collection abstraction and application to(…)

on YouTube ↗01h 02m

" summary

MemCAD implements a new sequence abstraction for unbounded sequences and plugs it into a reduced product of shape and value domains so the analyzer tracks list/tree shape plus lengths, extremal values and ordering. It is written functionally in OCaml with heavy use of functors (≈50 parametric modules), integrates into a C static analyser, and proves many functional-correctness properties (sorting, BST ops). It verifies a FreeRTOS-like microkernel instance (~1k LOC) with per-call times up to ~2 minutes, ~300s total for the suite, memory usage of a few GB; more precise but costlier than plain shape-only analyses.

AI-written summary · about

" chapters (8)

1. 0:00Introduction
2. 7:24Memory abstraction
3. 25:46Value properties
4. 30:01Collection abstractions
5. 47:23Functional correctness
6. 54:32Microkernel verification
7. 56:17Key takeaways and future directions
8. 56:40Q&A

" related talks

• 27mLightweight Shape Analysis based on Physical TypesMatthieu Lemerre, Xavier Rival, Olivier Nicole · VMCAI 2022
• 43mEverything I learned about static analysis and program safety in C++Sunny Chatterjee · Pure Virtual C++ 2022
• 32mSymbolic analysis by using folding narrowing with irreducibility and SMT constra...Santiago Escobar, Raúl López-Rueda, Julia Sapiña · FTSCS 2023
• 20mACES: Automatic Compartments for Embedded SystemsMathias Payer, Abraham A Clements, Naif Saleh Almakhdhub, Saurabh Bagchi · USENIX Security '18
• 49mCompiling to preserve our privacyManohar Jonnalagedda, Jakob Odersky · Scala Days Lausanne 2019
• 28mMemory simulations, security and optimization in a verified compilerDavid Monniaux · CPP 2024
• 29müberSpark: Enforcing Verifiable Object Abstractions for Automated...Limin Jia, Amit Vasudevan, Sagar Chaki, Petros Maniatis, Anupam Datta · USENIX Security '16
• 35mDeep-Kernel Treasure Hunt: Finding exploitable structures in the Linux kernelYudai Fujiwara · CODE BLUE 2023