K-State Center for Cybersecurity and Trustworthy Systems (K-CaTS)

Secure Software System Construction

Researchers in the SAnToS Laboratory - Dr. Hatcliff, Dr. Amtoft, and Dr. Robby develop compositional contract-based approaches for certifying secure information flow requirements. We collaborate with researchers from Rockwell Collins Advanced Technology Center (RC ATC) to develop compositional contract-based approaches for certifying secure information flow requirements in military information assurance products. Rockwell Collins is a leading manufacturer of avionics and communications solutions, both for commercial aviation and the military. Rockwell Collins Advanced Technology Center is Rockwell Collins' research and development center and supports the company by developing, acquiring, and transitioning technology into our product groups. Many Rockwell Collins product groups are currently developing products, or expect soon to develop products, that communicate with more than one security domain. Rockwell Collins markets products in a broad range of markets of interest to the DoD and U.S. Air Force, including communication, avionics, navigation systems, and displays offerings. The need to process information from diverse security domains with Multiple Levels of Security (MLS) is an increasingly common requirement across many of Rockwell Collins' diverse military businesses.

Computer security is clearly an area of pressing national need, and previous work of our own and others convinces us that application of automatic program analysis techniques has the potential to make a substantial contribution to improving the current situation. Security is also attractive from a strictly scientific point of view, because the problems are so difficult. In particular, computer security is nearly unique as an aspect of software quality for which an incomplete "engineering" solution is never enough. A single security vulnerability is all that is needed for an attacker to wreak havoc, which means that only complete solutions are really valuable. A characteristic of our research approach is to pursue simultaneously static, dynamic, specification-based, and hybrid approaches to eliminating security vulnerabilities.

We concentrate on two themes that we have chosen because we believe they present significant research challenges with a potentially high payoff:

  1. Security Specifications. We cannot begin to address many security issues without a specification defining what security means. We work on secure API's and disciplined styles of programming that reduce the likelihood of security flaws. We build tools for the static checking and dynamic monitoring of those security specifications. We are also currently developing techniques and tools for the inference of security specifications.
  2. Security Issues in Language Semantics. There are security problems that exist within a single program where the needed specification is already implicit in the language semantics. We investigate four problems that are pervasive today: (a) leakage of private data (confidentiality), (b) tainted data (integrity), (c) verification of security properties using off the shelf verifiers and theorem prover and (d) reasoning about security issues in scripting languages such as PHP, Ruby, Perl, Python.

Impact:

The scientific impact of this research is to further our ability to design, compose, and automatically verify secure software. Program analysis is an area that has seen great progress recently, but the design space of solutions that are combinations of static analysis, dynamic analysis, and user specification is enormous.

Successful research in software security has tremendous impact on society as a whole. It is obvious to all that the current state of security of our shared computing infrastructure is very low, and that despite this knowledge we are still unable to produce new software that is secure. Any techniques that make software more secure is therefore widely influential.

Representative Publications:

  1. Torben Amtoft, John Hatcliff, Edwin Rodriguez, Robby, Jonathan Hoag, and David Greve. Specification and checking of software contracts for conditional information flow. In Proceedings of the 15th International Symposium on Formal Methods (FM'08), pages 229--245, Springer LNCS 5014, May 2008.
  2. Torben Amtoft and Anindya Banerjee: Verification Condition Generation for Conditional Information Flow. In Proceedings of the ACM Workshop of Formal Methods in Security Engineering. June 2007.
  3. Torben Amtoft, Sruthi Bandhakavi and Anindya Banerjee: A Logic for Information Flow in Object-Oriented Programs. In Proceedings of 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). Charleston, SC, USA, 2006.
  4. Torben Amtoft and Anindya Banerjee. Information flow analysis in logical form. In Proc. SAS 2004, pages 100-115, Springer LNCS 3148, 2004. Received the SAS'04 Best Paper Award.
  5. Anindya Banerjee, David A. Naumann and Stan Rosenberg: Expressive Declassification Policies and their Modular Static Enforcement. In Proceedings of the 2008 IEEE Symposium on Security and Privacy. May 2008.
  6. Anindya Banerjee, David A. Naumann and Stan Rosenberg: Towards a Logical Account of Declassification. In Proceedings of the 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security. June 2007.
  7. Torben Amtoft and Anindya Banerjee: Verification Condition Generation for Conditional Information Flow. In Proceedings of the ACM Workshop of Formal Methods in Security Engineering. June 2007.
  8. Marco Pistoia, Anindya Banerjee and David A. Naumann: Beyond Stack Inspection: A Unified Access Control and Information Flow Security Model. In Proceedings of the 2007 IEEE Symposium on Security and Privacy. May 2007.
  9. Gurvan Le Guernic, Anindya Banerjee, Thomas Jensen and David A. Schmidt: Automata-based Confidentiality Monitoring. In Proceedings of the Eleventh Annual Asian Computing Science Conference. December 2006.
  10. Xianghua Deng, Robby, and John Hatcliff. Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs, Proceedings of the 2007 International Conference on Software Engineering and Formal Methods, September 2007.

Research Funding:

  1. ($50K; PI: Hatcliff; co-PI: Amtoft) from Rockwell Collins for the project "Information Flow Modeling and Analysis" where a key deliverable is to explore a language for conveniently describing precise, conditional information flow properties for software operating on heap-based data structures.
  2. "Automatic Control-Network Security Management Using Attack Graphs." US Department of Energy. $35K, 3/20/2007 - 8/17/2007
  3. CT-ISG: Model-Based, Automatic Network Security Management. National Science Foundation. $245K, 8/1/2007 -7/31/2009.
  4. REU:CT-ISG: Model-Based, Automatic Network Security Management. National Science Foundation. $6K, 8/1/2007 -7/31/2009.
  5. John Hatcliff (PI). Automatic Analysis Techniques for Discovering Information Flow Properties of Cryptographic Controllers (Rockwell Collins Advanced Technology Center). Amount: $85,000. Duration: October 2008 -- August 2009.
  6. John Hatcliff (PI), with Torben Amtoft, Simon Ou, and Robby. A Domain Specific Language for Defining High-Assurance Secure-Network Guards (Rockwell Collins Advanced Technology Center). $85,000. Duration: September 2008 -- August 2009.
  7. John Hatcliff (PI). Conditional Information Flow Modeling for High-assurance Systems (Rockwell Collins Advanced Technology Center). Amount: $25,000. Duration: October 2008 -- November 2008.
  8. John Hatcliff (PI) with Torben Amtoft on Information Flow Modeling Analysis (Formalization and Supporting Tools for Secure Information Flow Certification of Industrial Applications). (Rockwell Collins Advanced Technology Center). Amount: $50,000. Duration: Jan 2007 -- December 2007
  9. John Hatcliff (PI) with Torben Amtoft and Anindya Banerjee. An Integrated Specification and Verification Environment for Component-based Architectures of Large-scale Distributed Systems (Air Force Office of Scientific Research (AFOSR)). Amount: $448,530. Duration: April 2006 -- March 2009.
  10. Torben Amtoft, John Hatcliff, Edwin Rodriguez, Robby, Jonathan Hoag, and David Greve, "Specification and Checking of Software Contracts for Conditional Information Flow", Proceedings of the 2008 International Conference on Formal Methods (FM '08), LNCS 5014, May 2008.
  11. ($200K for 2006-2009; PI: Banerjee) from NSF (National Science Foundation) Cyber Trust program for the proposal "Access Control and Downgrading for Information Flow Assurance" which has verification of access control, information flow, downgrading, trust management as its key components
  12. ($150K/year for 2006-8; PI: Hatcliff; co-PI: Amtoft & Banerjee) from AFOSR (Air Force Office of Scientific Research) for the proposal "An Integrated Specification and Verification Environment for Component-based Architectures of Large-scale Distributed Systems" which has "Secure Information Flow" as one of its components.
  13. ($135K for 2003-2008, award total $900K) from NSF ITR. Co-PIs: Banerjee and Schmidt (K-State) with Alex Aiken, Thomas Henzinger, George Necula, Ras Bodik, and David Wagner, (University of California, Berkeley): Language-based Security.