C generic Team1 (E-ACSL) Benchmark1
Contents
Benchmark Data
This benchmark is located in crv.liflab.ca@/home/e-acsl/crv16_benchmarks/c-generic-track/integer-overflow
The Trace Part
E-ACSL has no notion of trace
The Property Part
Given integers A and B check if the sum of these integers is less than some integer C. This check should take into account the fact that expression (A + B) can overflow.
Informal Description
The benchmark provides a simple implementation of a utility that prints the contents of a file given by two C strings that store the directory the file is located in, and the base name of that file. The lengths of the strings are given as separate arguments.
The scenario explored by this benchmark is as follows. The strings representing a directory and a file name are concatenated in a fixed-size buffer. The concatenation is guarded by a conditional statement that adds the lengths of the strings and immediately returns if the sum of of the lengths is greater than the size of the buffer. The aim of the guard is to prevent writing past the bounds of the fixed-size buffer.
The design of the guard is flawed: large enough values of string lengths may cause the addition to overflow and wrap around to a low number. This allows to bypass the check and lead to a buffer overflow during string concatenation.
The final step reads data from a file and output its contents to the standard output stream.
Demonstration Traces
Formal Specification
The formal specification is given using ACSL
/*@ assert (a + b) <= max; */
where a, b and max are of integral types.
