Difference between revisions of "C implicit track"
(→Team 1 (E-ACSL)) |
(→Team 1 (E-ACSL)) |
||
| Line 32: | Line 32: | ||
Further information about E-ACSL can be found [http://frama-c.com/eacsl.html here]. | Further information about E-ACSL can be found [http://frama-c.com/eacsl.html here]. | ||
| + | |||
| + | * [[ C implicit Team0 Benchmark1 | Illegal heap dereference ]] | ||
| + | |||
| + | == Benchmark Data == | ||
| + | |||
| + | This benchmark is located in ''crv.liflab.ca@/home/e-acsl/crv16_benchmarks/c-implicit-track/heap-performance'' | ||
| + | |||
| + | === The Trace Part === | ||
| + | |||
| + | E-ACSL has no notion of trace | ||
| + | |||
| + | === The Property Part === | ||
| + | |||
| + | ==== Informal Description ==== | ||
| + | |||
| + | This benchmark relates to a property of memory safety and more specifically to a violation involving writing past the bounds of a heap-allocated memory block. | ||
| + | |||
| + | The main aim of this benchmark to evaluate performance of a dynamic verification tool in the presence of intensive memory allocation for a memory safety property involving the legality of writes to heap-allocated memory locations. | ||
| + | |||
| + | The scenario explored by this benchmark is as follows. Allocate a number of memory blocks on a program's heap and write to every byte of the allocated memory (potentially writing past the bounds of allocated memory). Deallocate heap memory. Repeat. | ||
| + | |||
| + | ==== Demonstration Traces ==== | ||
| + | |||
| + | ==== Formal Specification ==== | ||
| + | |||
| + | The formal property is given using the [http://frama-c.com/acsl.html ACSL] | ||
| + | |||
| + | Let '''p''' be a term of a pointer type, then: | ||
| + | |||
| + | /*@ assert \valid(p); */ | ||
| + | |||
| + | ==== A FO-LTL Specification ==== | ||
== Team 2 == | == Team 2 == | ||
Revision as of 16:29, 3 June 2016
The C implicit track is concerned with the monitoring of implicit properties of C programs. This is the first time we are running this track and want to be somewhat guided by the participants of the track. The idea is that programs will be submitted and general implicit properties (such as memory safety) should be checked.
Please follow the example of Team 0 in how to organise your submission i.e. provide a team name and description and create a page per benchmark (named Track TeamX BenchmarkY).
Please use the below template to create your benchmark Wiki pages. Do not modify the template.
Benchmark Template - C implicit track
Contents
Team 0 (ExampleName)
The ExampleName tool works by magic dust and hope, utilising a new constant time algorithm for sorting. This paragraph is an example of the fact that there should be a few sentences written about the team and its tool. The tool is developed by John Lennon and Tintin. Further information about the tool can be found at [1].
Team 1 (E-ACSL)
E-ACSL is both a formal specification language and a Frama-C plugin for runtime assertion checking of C code.
The E-ACSL specification language is an executable subset of the behavioral specification language for C programs called [http://frama- c.com/acsl.html ACSL]. E-ACSL supports function contracts, assertions, user-defined predicates and built-in predicates (like \valid(p) indicating that reading from or writing to a memory location pointed to by a pointer p is safe).
The E-ACSL Frama-C plugin E-ACSL Frama-C plugin automatically converts a given C program (say P) containing E-ACSL annotations into a program P' instrumented with assertions that verify E-ACSL properties at runtime.
E-ACSL is developed by the Software Security Laboratory at CEA LIST
Further information about E-ACSL can be found here.
Benchmark Data
This benchmark is located in crv.liflab.ca@/home/e-acsl/crv16_benchmarks/c-implicit-track/heap-performance
The Trace Part
E-ACSL has no notion of trace
The Property Part
Informal Description
This benchmark relates to a property of memory safety and more specifically to a violation involving writing past the bounds of a heap-allocated memory block.
The main aim of this benchmark to evaluate performance of a dynamic verification tool in the presence of intensive memory allocation for a memory safety property involving the legality of writes to heap-allocated memory locations.
The scenario explored by this benchmark is as follows. Allocate a number of memory blocks on a program's heap and write to every byte of the allocated memory (potentially writing past the bounds of allocated memory). Deallocate heap memory. Repeat.
Demonstration Traces
Formal Specification
The formal property is given using the ACSL
Let p be a term of a pointer type, then:
/*@ assert \valid(p); */
