Comparing Formal Verification and Hardware Checks for Achieving Memory Safety

@Unpublished{ talk:brucker:cheri-vs-verification:2024,
  author     = {Achim D. Brucker},
  date       = {2024-04-11},
  title      = {Comparing Formal Verification and Hardware Checks for
                Achieving Memory Safety},
  eventtitle = {Embedded World},
  language   = {english},
  areas      = {formal methods},
  venue      = {Nuremberg, Germany},
  abstract   = {Memory corruption vulnerabilities are one of the most common
                software security vulnerabilities. While in many application
                areas, the use of memory-safe languages is possible, this is
                often not the case for embedded systems or low-level
                implementations such as operating systems or network stacks.
                
                In this presentation, we discuss traditional approaches such
                as fuzzing, runtime pointer tracking, and formal verification
                and compare them with a novel hard-ware based solution. The
                latter is currently implemented in the Morello processor.
                
                The Morello processor is an experimental multicore,
                superscalar ARMv8-A processor, implemented as System-on-Chip
                that supported the Capability Hardware Enhanced RISC
                Instructions (CHERI) set. CHERI provides a fine-grained memory
                protection that allow historically memory-unsafe programming
                languages such as C and C++ to be adapted to provide strong,
                compatible, and efficient protection against many currently
                widely exploited vulnerabilities.
                
                We will conclude our presentation with a detailed comparison
                of advantages and disadvantages using a set of coding examples
                that have been derived from (vulnerable code taken from)
                several application domains. In particular, our examples are
                taken from vulnerabilities detected in various embedded tcp/ip
                stacks and from a software stack used in connected vehicles.
                
                This work was partly funded by the Innovate UK project
                AutoCHERI. },
  note       = {Author copy: \url{http://logicalhacking.com/publications/talk-brucker-cheri-vs-verification-2024/}},
}