Applications of Formal Methods and Related Techniques for Security

Our research has relied on formal methods and foundations to tackle several important problems in security. Our earliest work in this regard concerned the use of model-checking techniques for reasoning about vulnerabilities that arise due to misconfigurations. Rather than relying on a set of rules that enumerate the known causes of vulnerabilities, we developed a model-based approach that can automatically discover unknown vulnerabilities, and moreover, construct multi-step attacks that exploit these vulnerabilities.

Our model-carrying code relies on automated verification techniques to address the problem of security policy development for containing untrusted code. We developed an automata-based model-checking algorithm that computed the set of all counter examples, and used this as the basis for suggesting refinements to a basic security policy. Intuitively, this refinement captures a minimal relaxation of the base policy that would allow untrusted code to complete its task.

More recently, we have been interested in applying program analysis techniques for discovering software vulnerabilities, and for optimizing security-related program transformations.

Related Publications

[1]  WebSheets: Web Applications for Non-Programmers

Riccardo Pelizzi and R. Sekar
New Security Paradigms Workshop (NSPW) September, 2015.

[2]  Provably Correct Runtime Enforcement of Non-Interference Properties

V.N. Venkatakrishnan, Wei Xu, Daniel DuVarney and R. Sekar
International Conference on Information and Communications Security (ICICS) December, 2006. (Supercedes Technical Report SECLAB-04-01, Stony Brook University, March, 2004.).

[3]  Dataflow Anomaly Detection

Sandeep Bhatkar, Abhishek Chaturvedi and R. Sekar
IEEE Symposium on Security and Privacy (IEEE S&P) May, 2006. (Supercedes Technical Report SECLAB-05-03 Improving Attack Detection in Host-Based IDS by Learning Properties of System Call Arguments, July 2005.).

[4]  Model-Carrying Code: A Practical Approach for Safe Execution of Untrusted Applications

R. Sekar, V.N. Venkatakrishnan, Samik Basu, Sandeep Bhatkar and Daniel DuVarney
ACM Symposium on Operating Systems Principles (SOSP) October, 2003.

[5]  Generation of All Counter-Examples for Push-Down Systems

Samik Basu, Diptikalyan Saha, Yow-Jian Lin and Scott Smolka
Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE) June, 2003.

[6]  An approach for Secure Software Installation

V.N. Venkatakrishnan, R. Sekar, Sofia Tsipa, Tapan Kamat and Zhenkai Liang
USENIX Large Installation System Administration Conference (LISA) November, 2002.

[7]  Model-Based Analysis of Configuration Vulnerabilities

C.R. Ramakrishnan and R. Sekar
Journal of Computer Security (JCS) January, 2002.

[8]  Model-Carrying Code (MCC): A New Paradigm for Mobile-Code Security

R. Sekar, C.R. Ramakrishnan, I.V. Ramakrishnan and Scott Smolka
New Security Paradigms Workshop (NSPW) September, 2001.

[9]  Model-Based Analysis of Configuration Vulnerabilities

C.R. Ramakrishnan and R. Sekar
ACM CCS Workshop on Intrusion Detection Systems (WIDS) October, 2000.

[10]  Model-Based Vulnerability Analysis of Computer Systems

C.R. Ramakrishnan and R. Sekar
Verification, Model Checking, and Abstract Interpretation (VMCAI) September, 1998.

Research Areas

Research Problems

Local Search