Buffer overflow detection based on a synthesis of assertions from templates and k-induction

A system for buffer overflow detection, the system comprising:

• a computer processor;
• an assertion synthesis engine executing on the computer processor configured to:
• obtain a program code configured to access memory locations in a loop using a buffer index variable;
• obtain an assertion template configured to capture a dependency between the buffer index variable and a loop index variable of the loop in the program code;
• generate an assertion using the assertion template;
• an assertion verification engine executing on the computer processor configured to:
• verify that the assertion holds, using a k-induction comprising:
• making a determination that the assertion holds for k-1 iterations of the loop when executing the loop with constraints based on concrete values, and based on the determination:
• symbolizing the constraints,
• executing k-1 iterations of the loop using the symbolized constraints to obtain additional constraints,
• executing a single iteration of the loop using the symbolized constraints and the additional constraints, and
• based on a determination that the assertion holds for the single iteration, concluding that the assertions holds for all executions of the loop;
• and
• a buffer overflow detection engine executing on the computer processor configured to:
• determine whether a buffer overflow exists using the assertion.

A non-transitory computer readable medium comprising computer readable program code for causing a computer system to:

• obtain a program code configured to access memory locations in a loop using a buffer index variable;
• obtain an assertion template configured to capture a dependency between the buffer index variable and a loop index variable of the loop in the program code;
• generate an assertion using the assertion template;
• verify that the assertion holds, using a k-induction comprising:
• making a determination that the assertion holds for k-1 iterations of the loop when executing the loop with constraints based on concrete values, and based on the determination:
• symbolizing the constraints,
• executing k-1 iterations of the loop using the symbolized constraints to obtain additional constraints,
• executing a single iteration of the loop using the symbolized constraints and the additional constraints, and
• based on a determination that the assertion holds for the single iteration, concluding that the assertions holds for all executions of the loop;
• and
• determine whether a buffer overflow exists using the assertion.