Persistency Semantics for Verification under Ext4
Working with files, one can observe weak behaviors: the kernel, the file system, and the hardware affect the order and atomicity of the file operations. Besides similar effects observed in memory, the persistency problem arises: In which state are the files observed upon a crash recovery? Being poorly documented, modern filesystems are hardly understood by programmers, which leads to severe software bugs, such as data corruption.
As a first step towards solving this problem, the formal model of the Linux ext4 has been proposed. In the talk, we’ll cover this model and the extension of GenMC model checker algorithm , enabling one to verify software performing file I/O. In addition, there will be presented several bugs in commonly-used text editors (such as vim and nano) revealed by the algorithm.
Speaker: Ilya Kaisin
- About seminars
26 October 2020Representability of invariants of programs with algebraic data type
19 October 2020Step-indexing semantics of recursive types
12 October 2020Incorrectness Logic
5 October 2020Development of domain-specific compilers for specialized processors
28 September 2020Slightly subcubic algorithm for the context-free language reachability (CFL-reachability) problem