Interactive analysis of a security specification

Abstract

A downgrader in a computer program under test can be identified. 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, a test unit for the downgrader can be created using the counter example as an input parameter to the downgrader, and 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 prompt that prompts a user to simplify a model of the downgrader can be presented to the user.

1 - 24 . (canceled) 
     
     
         25 . A method, comprising:
 identifying a downgrader in a computer program under test;   performing, using a processor, 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; 
 creating a test unit for the downgrader using the counter example as an input parameter to the downgrader; and 
 executing the test unit to perform testing on the downgrader in a second level of analysis; and 
   responsive to the downgrader passing the testing performed in the second level of analysis, presenting to a user a prompt that prompts the user to simplify a model of the downgrader.   
     
     
         26 . The method of  claim 25 , wherein the executing the test unit to perform testing on the downgrader in the second level of analysis comprises:
 receiving from the user a user input to initiate execution of the test unit.   
     
     
         27 . The method of  claim 25 , wherein the automatically 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 corresponding to the downgrader within a call graph; and   feeding the first logical formula and the second logical formula into a string-analysis solver.   
     
     
         28 . The method of  claim 27 , further comprising determining whether the downgrader passed the testing performed in the second level of analysis by determining whether the string-analysis solver ran successfully using the first logical formula and the second logical formula. 
     
     
         29 . The method of  claim 28 , wherein the first logical formula is the counter example, the method further comprising:
 responsive to determining that the string-analysis solver ran successfully using the first logical formula and the second logical formula, determining that the first logical formula is valid as the counter example.   
     
     
         30 . The method of  claim 25 , wherein the performing testing on the downgrader in the first level of analysis comprises:
 building a call graph rooted at a method corresponding to the downgrader;   modeling instructions of the method corresponding to the downgrader within the call graph;   asserting a pattern with respect to return variables in the call graph having the modeled instructions; and   running a string-analysis solver on the pattern that is asserted.   
     
     
         31 . The method of  claim 30 , further comprising:
 determining whether the string-analysis solver ran successfully on the pattern that is asserted;   wherein the downgrader not passing the testing performed in the first level of analysis is determined by determining that the string-analysis solver did not run successfully on the pattern that is asserted.   
     
     
         32 . A system comprising:
 a hardware 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; 
 creating a test unit for the downgrader using the counter example as an input parameter to the downgrader; and 
 executing the test unit to perform testing on the downgrader in a second level of analysis; and 
   responsive to the downgrader passing the testing performed in the second level of analysis, presenting to a user a prompt that prompts the user to simplify a model of the downgrader.   
     
     
         33 . The system of  claim 32 , wherein the executing the test unit to perform testing on the downgrader in the second level of analysis comprises:
 receiving from the user a user input to initiate execution of the test unit.   
     
     
         34 . The system of  claim 32 , wherein the automatically 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 corresponding to the downgrader within a call graph; and   feeding the first logical formula and the second logical formula into a string-analysis solver.   
     
     
         35 . The system of  claim 34 , the executable operations further comprising determining whether the downgrader passed the testing performed in the second level of analysis by determining whether the string-analysis solver ran successfully using the first logical formula and the second logical formula. 
     
     
         36 . The system of  claim 35 , wherein the first logical formula is the counter example, the executable operations further comprising:
 responsive to determining that the string-analysis solver ran successfully using the first logical formula and the second logical formula, determining that the first logical formula is valid as the counter example.   
     
     
         37 . The system of  claim 32 , wherein the performing testing on the downgrader in the first level of analysis comprises:
 building a call graph rooted at a method corresponding to the downgrader;   modeling instructions of the method corresponding to the downgrader within the call graph;   asserting a pattern with respect to return variables in the call graph having the modeled instructions; and   running a string-analysis solver on the pattern that is asserted.   
     
     
         38 . The system of  claim 37 , the executable operations further comprising:
 determining whether the string-analysis solver ran successfully on the pattern that is asserted;   wherein the downgrader not passing the testing performed in the first level of analysis is determined by determining that the string-analysis solver did not run successfully on the pattern that is asserted.   
     
     
         39 . A computer program product, comprising:
 a computer readable storage medium having program code stored thereon, wherein the computer-readable storage device is not a transitory, propagating signal per se, the program code executable by a data processing system to initiate operations including:   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; 
 creating a test unit for the downgrader using the counter example as an input parameter to the downgrader; and 
 executing the test unit to perform testing on the downgrader in a second level of analysis; and 
   responsive to the downgrader passing the testing performed in the second level of analysis, presenting to a user a prompt that prompts the user to simplify a model of the downgrader.   
     
     
         40 . The computer program product of  claim 39 , wherein the executing the test unit to perform testing on the downgrader in the second level of analysis comprises:
 receiving from the user a user input to initiate execution of the test unit.   
     
     
         41 . The computer program product of  claim 39 , wherein the automatically 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 corresponding to the downgrader within a call graph; and   feeding the first logical formula and the second logical formula into a string-analysis solver.   
     
     
         42 . The computer program product of  claim 41 , the operations further comprising determining whether the downgrader passed the testing performed in the second level of analysis by determining whether the string-analysis solver ran successfully using the first logical formula and the second logical formula. 
     
     
         43 . The computer program product of  claim 42 , wherein the first logical formula is the counter example, the operations further comprising:
 responsive to determining that the string-analysis solver ran successfully using the first logical formula and the second logical formula, determining that the first logical formula is valid as the counter example.   
     
     
         44 . The computer program product of  claim 39 , wherein the performing testing on the downgrader in the first level of analysis comprises:
 building a call graph rooted at a method corresponding to the downgrader;   modeling instructions of the method corresponding to the downgrader within the call graph;   asserting a pattern with respect to return variables in the call graph having the modeled instructions; and   running a string-analysis solver on the pattern that is asserted.