Formal Verification – Security Checking

Conference: FV2016 (click here to see full programme)
Speaker: Elchanan Rappaport, President
Organisation: Gila Logic
Presentation Title: Formal Verification – Security Checking
Abstract: Secure architectures are becoming more complex. They route secure and non-secure data over the same channels, and share the same resources, but still require that there be no leakage from one domain to the other. Simulation provides no method[s?] for confirming that secure data is respected.

We present Formal methods and techniques, as well as actual user cases, which demonstrate how Formal successfully addresses this verification problem.

  • Secure Architectures are not as trivial as we’d like.
  • Simulation has no way to test them!
  • We show how Formal has many methods to address Design Security.
Speaker Bio: Elchanan Rappaport is the founder of Gila Logic, Inc. He has 35 years of experience in both simulation and formal-based verification, having worked with a number of semiconductor companies, including IBM, ARM, TI, National, Microsoft and others. For the last 15 years he has focused on high-end formal verification projects and is a common speaker at formal conferences and events.

Presentation Material: