Formal methods offer a way out of this arms race. Based on mathematically precise system and attacker models, we can systematically eliminate entire classes of attack strategies. With recent advances in logic and automated reasoning, the application can even be largely 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, striving for computer-aided analysis and construction of secure systems with the strongest possible formal guarantees. This includes the development of methods for achieving rigorous security guarantees for systems and software, runtime methods for monitoring and enforcement, design-time methods for static analysis and program repair, and a comprehensive methodology for building secure large-scale systems from small secure building blocks.
LNCS19th International Symposium on Automated Technology for Verification and Analysis (ATVA 2021)
Proceedings of the IEEE/CVF International Conference on Computer Vision (ICCV)IEEE International Conference on Computer Vision (ICCV), 2021
30th USENIX Security Symposium (USENIX Security 21)30th USENIX Security Symposium (USENIX Security 21)
iX Magazin für professionelle Informationstechnik
Proceedings, Part I33rd International Conference, CAV 2021