secappdev.org's video: Between Testing and Formal Verification - Jan Tobias Muehlberg

The security testing of software is inherently difficult. This is because vulnerabilities typically emerge as unanticipated interactions in the design of a software component, as implementation artefacts that were not specified in the design, or as bugs, where design and implementation deviate. Thus, when searching for breaches of security properties we are looking for design or implementation details that can be abused in ways not considered by the designers, developers and testers of a software component. Formal methods promise to systematise this search for needles in haystacks and use mathematical rigour to provide convincing arguments for the absence of such needles. Yet, with few exceptions in safety-critical systems engineering, the adoption of formal techniques in software development processes is low. Furthermore, formal methods traditionally focus on safety aspects of software, i.e., functional correctness and the absence of runtime exceptions of software. In this talk I will outline the advantages and disadvantages of modern approaches to formal software analysis and verification. I will focus on tools and techniques that can be integrated efficiently with testing efforts, in particular in security testing. Jan Tobias Muehlberg work as a researcher at imec-DistriNet, KU Leuven (BE). I am active in the fields of software security, and formal verification and validation of software systems, specifically for embedded systems and low-level operating system components. I am particularly interested in security architectures for safety-critical embedded systems and for the Internet of Things.