Interactive analysis of a security specification

摘要

Analyzing a security specification. An embodiment can include identifying a downgrader in a computer program under test. Testing on the downgrader can be performed in a first level of analysis. Responsive to the downgrader not passing the testing performed in the first level of analysis, a counter example for the downgrader can be automatically synthesized. Further, a test unit can be created for the downgrader using the counter example as an input parameter to the downgrader. The test unit can be executed to perform testing on the downgrader in a second level of analysis. Responsive to the downgrader passing the testing performed in the second level of analysis, a user can be prompted to simplify a model of the downgrader.

主权项

1. A system comprising:
a processor configured to initiate executable operations comprising: identifying a downgrader in a computer program under test; performing testing on the downgrader in a first level of analysis; responsive to the downgrader not passing the testing performed in the first level of analysis:
automatically synthesizing a counter example for the downgrader, wherein synthesizing the counter example for the downgrader comprises encoding as a first logical formula a complement of a regular pattern asserting a security property of a method corresponding to the downgrader, encoding as a second logical formula instructions of the method within a call graph, and feeding the first logical formula and the second logical formula into a string-analysis solver;creating a test unit for the downgrader using the counter example as an input parameter to the downgrader; andexecuting the test unit to perform testing on the downgrader in a second level of analysis.