CProver manual
|
The Symbolic Shadow Memory module described below is an implementation of what is outlined in the paper CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory.
CBMC implements Symbolic Shadow Memory. Symbolic Shadow Memory (from now on, SSM) allows one to create a parallel memory structure that is maintained by the analysis program and that shadows the standard memory of the program. In the Shadow Memory structure, a user can create fields, for which he can get (retrieve) and set values.
By doing so, a user can organise their own tracking of metadata related to the code, in a way that is then considered by the backend of CBMC during analysis. This can be used to implement novel analyses that the CBMC framework itself does not support. For example, the paper above presents as an example a taint analysis implemented with the use of the SSM component described here.
A user can interact with the Symbolic Shadow Memory component through four CBMC primitives. These allow the declaration of shadow memory fields, and get/set their corresponding values:
__CPROVER_field_decl_local
__CPROVER_field_decl_global
__CPROVER_get_field
__CPROVER_set_field
More precisely, their signatures (in pseudo-C, because of some constraints that we cannot express using the type system), along with some small examples of their usage, are described below:
Type constraints:
type1
: string literal, such as "field"
,SSM_value_type
: any value up to 8 bits in size (signed or unsigned).Declares a local shadow memory field called field_name
, and initialises it with the value init_value
. The field is going to be associated with function local-scope objects (i.e. a variable on the stack).
Note that each function scope will have a separate local shadow memory, so the value stored in the local shadow memory is not propagated to subcalls (even when the call is recursive). For this reason, to be able to access shadow memory argument values from a called function or the value of the return from the callee it is necessary to use the global shadow memory and passing arguments and return values as pointers or to use global variables.
Type constraints:
type1
: string literal, such as "field"
,SSM_value_type
: any value up to 8 bits in size (signed or unsigned).As for __CPROVER_field_decl_local
, but the field declared is associated with objects whose lifetime exceeds the current function scope (i.e. global variables or heap allocated objects).
Type constraints:
SSM_VALUE_TYPE
: the type of the returned value is the same of the SSM field, i.e. the type that was used to intialise the SSM field during declaration,type1 *
: a non-void
pointer to an object of type type1
, whose address we are going to use for indexing the shadow memory component for the field declared,type2
: a string literal-typed value, denoting the name of the field whose value we want to retrieve, such as "field"
.Retrieves the latest value associated with a SSM field to the given pointer. This would be either the value the field was declared to be initialised with, or, if there had been subsequent changes to it through a __CPROVER_set_field
(see __CPROVER_set_field
section below), the value that it was last set
with.
Note that getting the value of a local variable from a global SSM field or the opposite will return the default value for that SSM field (and it will not fail).
Type constraints:
type1 *
: a non-void
pointer to an object of type type1
, whose address we are going to use for indexing the shadow memory component for the field declared,type2
: a string literal-typed value, denoting the name of the field whose value we want to retrieve, such as "field"
,type3
: type of the value to be set. This can be any integer type signed or unsigned (including _Bool
). Notice that if this type differs from the type the SSM field was declared with (SSM_VALUE_TYPE
above) it will be implicitly casted to it.Sets the value associated with a SSM field to the given pointer p
with the given value set_value
. If the set_value
type is not the SSM_VALUE_TYPE
, it will be implicitly casted to it.
Note that setting the value of a local variable from a global SSM field or the opposite will produce no effect (and it will not fail).
When using SSM on compound type pointers (e.g. struct
and union
) the value used for the __CPROVER_set_field
will be replicated in each of the fields of the type, and aggregated again when retrieving them with __CPROVER_get_field
. The aggregation function is or
for an SSM field of _Bool
type, and max
for other types.
This is helpful, for example, in the case of taint analysis (as presented in the paper and shown below). In this case, when retrieving the taint value of a struct containing a tainted field the result value will indicate taint (without the need for changing non-tainted field values), and when setting the taint value of a struct then all its fields will be set to the given value.
Last modified: 2024-11-12 09:30:37 +0200