Automated tools for building secure software programs

摘要

A computer implemented tool is described that includes an assertion generator module that can automatically generate assertions, which are usable to verify application-specific security properties, for a computer software program. An assertion checker module can automatically analyze the computer software program to ensure that it satisfies the application-specific security properties. A graphical user interface module can display feedback to diagnose security flaws detected in the computer software program based on the analysis by the assertion checker module. In support of these modules are a code preprocessor module that can translate source code of the computer software program into an intermediate abstract representation, and a database module that can store the generated assertions and associated data in a database. Each of the modules can provide functionality at any time during code construction of the computer software program.

主权项

1. A computer implemented method for providing feedback concerning application-specific security properties for a computer software program, comprising the steps of:
automatically generating assertions that are desired to be valid, via one or more processors, based on desired application-specific security properties, validity of the assertions being usable to verify the application-specific security properties for the computer software program; automatically generating assertions that are known to be valid, via said or another one or more processors, based on the computer software program and received desired application-specific security properties; automatically analyzing the computer software program source code, via said or another one or more processors, to determine whether the computer software program satisfies the application-specific security properties, based on the automatically generated assertions that are desired to be valid, in combination with the automatically generated assertions that are known to be valid; generating feedback, via said or another one or more processors and based on determinations made in the step of automatically analyzing the computer software program, indicating instances of failure of the computer software program to satisfy the application-specific security properties; and displaying the feedback with a graphical user interface.