TAMIS: Threat Analysis and Mitigation for Information Security


Systems security requires both formal and engineering techniques to assess or even secure systems.  Modern systems are networked, use virtual machines to improve security and handle multiple applications concurrently on the same hardware, which is often enhanced to with hardware security modules. The resulting complexity is typically far beyond what formal verification techniques can manage.  On the other hand, merely applying engineering techniques to build secure systems has consistently resulted in deployments riddled with significant vulnerabilities.  TAMIS’s central goal is thus to demonstrably narrow the gap between the vulnerabilities found using formal verification and the issues found using systems engineering. Type theory is a representative example where formal verification and software engineering are combined, as in type theory formal methods are used to formally prove the absence of certain classes of bugs.  However, it is not the case that the entire system is shown to be formally correct with respect to a more comprehensive specification, which requires software engineering effort to handle classes of bugs not captured by the type system. In the next four years, we aim at creating tool chains that combine statistical model checking, abstract interpretation, supervised execution and manual annotations to efficiently check interesting security properties of realistic systems that were previously not efficiently checkable. We will establish a strong connection with industry and with international teams recognized in this area.

Research directions

  • Vulnerability analysis

    • The engineering view, and experience acquirement

    • Formal approaches for vulnerability analysis

    • Hardware vulnerability analysis
  • Malware analysis

    • Behavioral Malware Analysis

    • Malware and Signature Generation

    • Fault enabled malware

  • Secured payment system