Practical Verification of System-Software Components Written in Standard C
Speaker
Can Cebeci
EPFL
Host
Derek Leung
MIT CSAIL
Abstract:
Systems code is challenging to verify, because it uses constructs (like raw pointers, pointer arithmetic, and bit twiddling) that are hard for tools to reason about. Existing approaches either sacrifice programmer friendliness, by demanding significant manual effort and verification expertise, or generality, by restricting the programming language or requiring that the code adapt to the verification tool.
We identify a new point in the design space of verifiers that enables a different set of trade-offs, which prove practical in the context of verifying critical system components. We use several novel techniques to develop the TPot verification framework, targeted specifically at systems code written in C. With TPot, developers verify critical components they implement in standard, unrestricted C, using a C-based language to write “proof-oriented tests” (POTs) that specify the desired behavior. TPot then runs the POTs to prove correctness. We evaluate TPot on 6 different systems code bases, and show that it can verify them at the same level as 4 state-of-the-art verifiers, while consistently reducing the annotation burden, ranging up to more than 3×. TPot does not require these code bases to be adapted for verification and achieves verification times compatible with typical continuous-integration workflows.
Bio:
Can Cebeci is a fourth-year PhD student at EPFL, where he is co-advised by Prof. George Candea and Prof. Clément Pit-Claudel. His early PhD work is on designing practical abstractions and workflows for low-effort verification of low-level systems code. To this end, he has tinkered with memory models and stable SMT encodings for symbolic execution. His current interests are centered around demystifying SMT performance in order to understand and address solver explosion systematically.
Systems code is challenging to verify, because it uses constructs (like raw pointers, pointer arithmetic, and bit twiddling) that are hard for tools to reason about. Existing approaches either sacrifice programmer friendliness, by demanding significant manual effort and verification expertise, or generality, by restricting the programming language or requiring that the code adapt to the verification tool.
We identify a new point in the design space of verifiers that enables a different set of trade-offs, which prove practical in the context of verifying critical system components. We use several novel techniques to develop the TPot verification framework, targeted specifically at systems code written in C. With TPot, developers verify critical components they implement in standard, unrestricted C, using a C-based language to write “proof-oriented tests” (POTs) that specify the desired behavior. TPot then runs the POTs to prove correctness. We evaluate TPot on 6 different systems code bases, and show that it can verify them at the same level as 4 state-of-the-art verifiers, while consistently reducing the annotation burden, ranging up to more than 3×. TPot does not require these code bases to be adapted for verification and achieves verification times compatible with typical continuous-integration workflows.
Bio:
Can Cebeci is a fourth-year PhD student at EPFL, where he is co-advised by Prof. George Candea and Prof. Clément Pit-Claudel. His early PhD work is on designing practical abstractions and workflows for low-effort verification of low-level systems code. To this end, he has tinkered with memory models and stable SMT encodings for symbolic execution. His current interests are centered around demystifying SMT performance in order to understand and address solver explosion systematically.