# US 11,030,304 B2 · Buffer overflow detection based on a synthesis of assertions from templates and k-induction

> Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt

- Number: US 11,030,304 B2
- Document ID: US11030304B2
- Status: Granted
- Kind: B2
- Application number: 16/050,828
- Filed: 2018-07-31
- Published: 2020-02-06
- Granted: 2021-06-08
- Earliest claimed: 2018-07-31
- Assignees: Oracle International Corporation
- Applicants: Oracle International Corporation
- Inventors: Francois Gauthier; Nathan Keynes; Padmanabhan Krishnan; Cristina Cifuentes; Trung Quang Ta
- Web page: https://patentgrep.com/patent/US11030304B2

## CPC

- G06F 21/52: during program execution, e.g. stack integrity {; Preventing unwanted data erasure; Buffer overflow}
- G06F 8/433: {Dependency analysis; Data or control flow analysis}
- G06F 8/436: {Semantic checking}
- G06F 8/452: {Loops}
- G06F 11/3608: {using formal methods, e.g. model checking, abstract interpretation (theorem proving G06N5/013)}
- G06F 11/3636: {by tracing the execution of the program}
- G06F 9/5016: {the resource being the memory}
- G06F 2221/033: Test or assess software
- G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N)

## Abstract

A method for buffer overflow detection involves obtaining a program code configured to access memory locations in a loop using a buffer index variable, obtaining 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, generating an assertion using the assertion template, verifying that the assertion holds using a k-induction; and determining whether a buffer overflow exists using the assertion.

## Claims

### Claim 1

A method for buffer overflow detection comprising:
obtaining a program code configured to access memory locations in a loop using a buffer index variable;
obtaining 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;
generating an assertion using the assertion template;
verifying 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
determining whether a buffer overflow exists using the assertion.

### Claim 2 (depends on 1)

The method of claim 1, wherein determining whether the buffer overflow exists comprises making a determination, using the assertion and a memory allocation specified in the program code, that an execution of the program results in the buffer index variable to point to a memory location beyond the memory allocation during at least one execution of the loop.

### Claim 3 (depends on 1)

The method of claim 1,
wherein the assertion template and the assertion are for an upper bound of the buffer index variable, and
wherein a second assertion template is used to generate a second assertion for a lower bound of the buffer index variable.

### Claim 4 (depends on 1)

The method of claim 1, wherein the assertion template establishes a linear relationship between the buffer index variable and the loop index variable.

### Claim 5 (depends on 1)

The method of claim 1,
wherein the generated assertion establishes a boundary for the buffer index variable, based on the loop index variable, and
wherein the generated assertion, prior to verifying the assertion, is assumed to, but not known to, hold.

### Claim 6 (depends on 1)

The method of claim 1, wherein generating the assertion comprises:
obtaining first constraints using concrete values by executing k-1 iterations of the loop, wherein with each iteration, the assertion template is instantiated; and
solving the first constraints to obtain the assertion.

### Claim 7 (depends on 6)

The method of claim 6, further comprising:
making a determination, when verifying the assertion, that the assertion does not hold, and based on the determination:
obtaining second constraints using symbolic values by executing k-1 iterations of the loop, wherein with each iteration, the assertion template is instantiated; and
solving the second constraints to obtain the assertion.

### Claim 8

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.

### Claim 9 (depends on 8)

The system of claim 8, wherein determining whether the buffer overflow exists comprises making a determination, using the assertion and a memory allocation specified in the program code, that an execution of the program results in the buffer index variable to point to a memory location beyond the memory allocation during at least one execution of the loop.

### Claim 10 (depends on 8)

The system of claim 8,
wherein the generated assertion establishes a boundary for the buffer index variable, based on the loop index variable, and
wherein the generated assertion, prior to verifying the assertion, is assumed to, but not known to, hold.

### Claim 11 (depends on 8)

The system of claim 8, wherein generating the assertion comprises:
obtaining first constraints using concrete values by executing k-1 iterations of the loop, wherein with each iteration, the assertion template is instantiated; and
solving the first constraints to obtain the assertion.

### Claim 12 (depends on 11)

The system of claim 11, further comprising:
making a determination, when verifying the assertion, that the assertion does not hold, and based on the determination:
obtaining second constraints using symbolic values by executing k-1 iterations of the loop, wherein with each iteration, the assertion template is instantiated; and
solving the second constraints to obtain the assertion.

### Claim 13

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.

### Claim 14 (depends on 13)

The non-transitory computer readable medium of claim 13, wherein determining whether the buffer overflow exists comprises making a determination, using the assertion and a memory allocation specified in the program code, that an execution of the program results in the buffer index variable to point to a memory location beyond the memory allocation during at least one execution of the loop.

### Claim 15 (depends on 13)

The non-transitory computer readable medium of claim 13,
wherein the generated assertion establishes a boundary for the buffer index variable, based on the loop index variable, and
wherein the generated assertion, prior to verifying the assertion, is assumed to, but not known to, hold.

### Claim 16 (depends on 13)

The non-transitory computer readable medium of claim 13, wherein generating the assertion comprises:
obtaining first constraints using concrete values by executing k-1 iterations of the loop, wherein with each iteration, the assertion template is instantiated; and
solving the first constraints to obtain the assertion.

### Claim 17 (depends on 16)

The non-transitory computer readable medium of claim 16, further comprising:
making a determination, when verifying the assertion, that the assertion does not hold, and based on the determination:
obtaining second constraints using symbolic values by executing k-1 iterations of the loop, wherein with each iteration, the assertion template is instantiated; and
solving the second constraints to obtain the assertion.