Lightweight formal methods for software security testing automation
Development of high assurance secure computer systems has proven to be a challenging task. The primary approach to achieving high assurance is the application of formal methods. Applied to security, formal methods are particularly complex as security requirements mostly state what must not happen. There is no single tool or verification system that is suitable across the entire combined hardware and software product life cycle – and none have the industrial quality or full range of capabilities needed for the production of high assurance secure systems.

Testing is a significant element in the production of high assurance systems, and it is still a major practical element for ensuring software correctness. Nevertheless, current testing technologies are labor intensive and lack a formal basis, so that comprehensive testing can seriously impede the time to market of new products. To address these problems, this project will develop automated tools for software security testing.

DoD is currently seeking security architectures that combine the enforcement of dynamic security policies with the use of commercial computer and communications products. In many contexts these elements must protect information with a high assurance against unauthorized access. This research will provide advances in testing specifically targeted for next generation dynamically-configurable separation kernels, and on creating tools that will promote rapid, as well as significantly improved testing cycles.

The above diagram provides a high-level view of the suggested approach. For test case generation, we suggest environment models for generating test scenarios and extracting test drivers from them. A pseudo-random test driver extracted from the scenario provides for inputs to the System Under Test (SUT) and may also intercept outputs from the SUT for behavior monitoring. However, in the high volume of tests required for high assurance system development, it is labor intensive to identify test results that deviate from the expected results. If the set of properties for which inspection is performed is carefully defined, then it is possible for an automated mechanism to monitor test results. To this end, security properties will be specified in a domain-specific formal language supported by a tool that can translate those specifications into run-time SUT instrumentation for monitoring the results of the test run. Hence, the whole testing process will be supported by automation tools.
 
Project Leads
Cynthia Irvine, Naval Postgraduate School
Mikhail Auguston, NPS
Timothy Levin, NPS

Return to Projects list


The National Center for Advanced Secure Systems Research NCASSR) at the University of Illinois at Urbana-Champaign (UIUC) is a multi-institutional cybersecurity research team. NCASSR focuses basic and applied research necessary to develop next generation information security technologies that address national cybersecurity needs. NCASSR is led by the National Center for Supercomputing Applications (NCSA) and supported by funding from the Office of Naval Research (ONR).


SELS 0.7 released
Secure Email List Services (SELS) is an open source software for creating and developing secure email list services among user communities.
 
Strong community engagement strengthens cybersecurity research and development
NCASSR-supported exploratory research at NCSA and elsewhere has sparked additional external funding and development opportunities as well as successful deployment and adoption by users ranging from the defense sector to state law enforcement to the utilities industry.
 
NCASSR Collaborator Goes To Washington
Carl Gunter, a professor in the University of Illinois Department of Computer Science and a project lead on NCASSR-supported work involving adaptive, secure messaging, recently spoke to an audience of congressional staffers and lobbyists on Capitol Hill regarding ways to address a variety of critical cybersecurity issues in areas such as healthcare and energy distribution.