SATMC is a SAT-based bounded model checker for security-critical systems that stems from a successful combination of encoding techniques originally developed for planning with others developed for the analysis of reactive systems. SATMC has been successfully applied in variety of application domains (security protocols, security-sensitive business processes, and cryptographic APIs) and for different purposes (design-time security analysis and security testing). SATMC strikes a balance between general purpose model checkers and security protocol analyzers as witnessed by a number of important success stories including the discovery of a serious man-in-the-middle attack on the SAML-based Single Sign-On (SSO) for Google Apps, an authentication flaw in the SAML 2.0 Web Browser SSO Profile, and a number of attacks on PKCS#11 Security Tokens. SATMC is integrated and used as back-end in a number of research prototypes (e.g. the AVISPA Tool, Tookan, the SPaCIoS Tool) and industrial-strength tools (e.g. the Security Validator plugin for SAP NetWeaver BPM).
The sophistication of software systems and the safety requirements posed by the increasingly complex environments they operate in call for higher and higher degrees of reliability. These requirements must be achieved precisely (i.e. not only at the design level, but also in the actual implementation). This calls for automated and effective verification techniques in the software development cycle. In this context Software Model Checking has recently become one of the leading approaches to automatic program analysis.
We contributed to the development of two software model checking techniques and tools: Symbolic model checking based of programs manipulating numeric data and arrays SMT-based bounded model checking of programsTools: Eureka, SMT-CBMC.
Decision procedures are key components of verification tools. We have contributed to the development of a number of techniques for the synthesis, integration and combination of decision procedures for a variety of (decidable) theories of practical interest.