SecProve: Analyzing Software for Security During Construction

Abstract:

SecProve is a prototype tool, designed and currently being implemented at the Naval Research Laboratory, for analyzing software for global security properties using local, automatically generated code assertions.  This technique permits SecProve to handle properties beyond the application-independent ones (e.g., “no buffer overflow”) treated by other tools.   SecProve’s generated assertions are of two classes: Class 1 (known to be valid or derivatively valid) and Class 2 (desired to be valid).  Verification of a global property is typically done by verifying the Class 2 assertions generated from that property.  A Class 2 assertion can be verified using Class 1 assertions plus verification of any Class 2 assertions on which those Class 1 assertions depend.  SecProve automatically generates assertions based on three sources: 1) developer annotations and function/procedure contracts (provided by the developer or automatically generated themselves), 2) the source code itself, using forward propagation, and 3) property specifications.  The use of forward propagation of assertions allows code to be analyzed as, rather than after, it is constructed.

To make it possible to generate assertions from a property, SecProve provides templates for specifying properties of certain classes. Each template is accompanied by its own assertion-generation scheme.  Thus, addition of a new property template to SecProve requires the extension of SecProve’s overall assertion generation scheme.  For each template, assertions are generated in two phases.  The first phase, which generates mostly those Class 2 assertions on which the property depends, is done by placement of assertions.  The second phase, which mostly generates Class 1 assertions, uses forward propagation of assertions.

Any property specification template included in SecProve may include slots for one or more predicates or functions that will be used to capture history information.  Currently, SecProve has templates for properties from three classes: dataflow, sanitization, and nonbypassability. The template for the sanitization property has a slot for a sanitized predicate that, applied to variable x, is used to express that x is “clean” as opposed to “dirty”.   Used by every dataflow property is a to function built into SecProve that, applied to a program variable x, captures the set of program variables from which content has flowed to x.   The semantics of the predicates and functions is defined not explicitly, but implicitly through the placement and forward propagation schemes for assertions involving the values of these predicates and functions.  Thus, forward propagation updates to and sanitized in the “obvious” way to reflect their intended meanings.

In programs with sufficiently complex conditional branches, it may be necessary to incorporate a mechanical theorem prover into SecProve to perform assertion checking.  However, in our examples so far, many of the Class 2 assertions to be checked capture simple history, and heavy duty theorem proving is not needed to check them.  Our current focus is on implementing straightforward assertion checking for simple history assertions.  The architecture of SecProve—which includes a source code preprocessor, the assertion generator, the assertion checker, a GUI, and a database through which these components communicate—has been described in [1].  A patent application [2] was filed for SecProve in January, 2014.  This poster will focus on the current status of  (and plans for) SecProve and walk through a user scenario.

[1] M. M. Archer, E. I. Leonard, and C. L. Heitmeyer. Idea: Writing secure C programs with SecProve. In J. Jürjens, B. Livshits, and R. Scandariato, editors, Proc. 5th Int’l Symp. on Engineering Secure Software and Systems (ESSoS 2013), volume 7781 of LNCS, pages 171–180. Springer, 2013.

[2] M. Archer, C. Heitmeyer, E. Leonard, C. Gasarch, and W. Ding. Automated tools for building secure software programs. U.S. Patent Application Number 14/163523, filed January 24, 2014 (pending).

Biography:

Dr. Myla Archer has been employed as a Computer Scientist at the U. S. Naval Research Laboratory since 1995. She received her A.B. in Mathematics from Knox College in 1963, A.M. in Mathematics from Harvard University in 1964, and Ph.D. in Computer Science from the University of Illinois in Urbana- Champaign in 1988. She taught Mathematics at Wheaton College in Norton, MA, and Computer Science at the University of California, Davis prior to coming to the NRL. Her main research interests include formal methods, specification and verification, automatic theorem proving, and software engineering. Dr. Archer has been involved in the organization of a number of conferences and workshops, including serving as general chair of TPHOLs (Theorem Proving in Higher Order Logics) in 1991 and as co-organizer of the STRATA workshop (on Design and Application of Strategies/Tactics in Higher Order Logics) in Rome, Italy in 2003. Dr. Archer is the principal developer of TAME (Timed Automata Modeling Environment), an interface to PVS for proving invariant and other properties of Timed Automata that can be used as a stand-alone tool or to provide theorem proving capabilities to other tools including NRL's SCR toolset and MIT's (Veromodo's) Tempo toolkit. Along with her NRL colleagues Elizabeth Leonard, Constance Heitmeyer, and Carolyn Gasarch and with Prof. Wei Ding of the University of Massachusetts, Boston, Dr. Archer has been developing SecProve, a toolset that supports analysis of source code for security properties while it is under construction by way of generating and checking invariant assertions in the code.