The CISPA Building

The fragile security of today's IT infrastructure is the result of a perpetuous arms race between attackers and defenders. Just as the defenders continuously improve their ability to tackle attacks, the attackers keep devising new malicious practices, refining classic attacks on programming errors as well as exploiting a broadening attack surface including routers, firmware, and the Internet of Things. There is a dire need for a fundamental shift in the basic approach to software security. Without such a shift, the attackers are always one step ahead of the defenders. Formal methods offer a way out of the arms race. Based on mathematically precise system and attacker models, formal methods systematically eliminate entire classes of attack strategies. With recent advances in logic and automated reasoning, the application of formal methods can largely be automated. Too often, however, formal methods are based on abstract system models and thus leave gaps that are not considered in these models. This research area aims for a phase transition in the scope and practical applicability of formal methods, ultimately striving for a holistic methodology for the computer-aided analysis and construction of secure systems with the strongest possible formal guarantees. This includes the development of methods and tools for achieving trustworthy, mathematically rigorous security guarantees for systems and software, runtime methods for monitoring and enforcement as well as design-time methods for static analysis and program repair, and a comprehensive methodology for conceptually building secure, large-scale systems from small secure building blocks, in particular including cryptographic operations.


Most Recent Publications

Title Date Authors Meta
Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity  2018  2018   Swen Jacobs, Mouhammad Sakr,  Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Proceedings