CERIAS - Center for Education and Research in Information Assurance and Security

Skip Navigation
Purdue University - Discovery Park
Center for Education and Research in Information Assurance and Security

Applying Formal Verification Techniques for Checking Compliance of Computer Systems and Protocols

Omar Chowdhury

Omar Chowdhury - Purdue University

Sep 30, 2015

Watch on Youtube Watch on YouTube


While designing computer systems and their underlying protocols, architects impose functionality, security, and privacy requirements or policies with which the designed systems and protocols should comply with. These requirements and policies are generally written in natural language and more often than not they are not complied with in the implementations due to ambiguity, misinterpretation of the requirements, or developer errors. Non-compliance with the requirements can not only have security, privacy, and utility consequences but also can have safety implications. One possible solution is to express the requirements in some formal language. In addition to eliminating ambiguities and misinterpretations of the requirements, this also enables application of formal verification techniques to check for compliance of the implementation against the desired requirements or the policies. Formal verification techniques can be applied for checking compliance in potentially three different settings. In the first setting,compliance checking is performed statically before a system or a protocol is deployed. In the second setting, a runtime monitor can be deployed alongside the system or the protocol, and the monitor provably disallows the system or the protocol to take non-compliant actions. Finally, compliance can be be checked in a post-hoc fashion by capturing all the relevant runtime events in an audit log which can then be scrutinized for non-compliance. In this talk, I will present demonstrative examples of using formal verification techniques for compliance checking in each of these settings.

About the Speaker

Omar Chowdhury is a Post-Doctoral Research Associate at the Department of Computer Science at Purdue University. Before joining Purdue, he was a Post-doctoral Research Associate at Cylab, Carnegie Mellon University. He received his Ph.D. in Computer Science from the University of Texas at San Antonio. His research interest broadly lies in the field of Computer Security and Privacy. He is specifically interested in applying formal verification techniques for developing efficient compliance checking mechanism for computer information systems with respect to applicable privacy regulations like HIPAA and GLBA. He has won the best paper award The ACM Symposium on Access Control Models and Technologies (SACMAT). He has also served as a program committee member in ACM SACMAT and ACM CCS.

Unless otherwise noted, the security seminar is held on Wednesdays at 4:30P.M. STEW G52 (Suite 050B), West Lafayette Campus. More information...


The views, opinions and assumptions expressed in these videos are those of the presenter and do not necessarily reflect the official policy or position of CERIAS or Purdue University. All content included in these videos, are the property of Purdue University, the presenter and/or the presenter’s organization, and protected by U.S. and international copyright laws. The collection, arrangement and assembly of all content in these videos and on the hosting website exclusive property of Purdue University. You may not copy, reproduce, distribute, publish, display, perform, modify, create derivative works, transmit, or in any other way exploit any part of copyrighted material without permission from CERIAS, Purdue University.