TagAnalysis

Overview

Tag analysis keeps track of data flows between memory locations. The analysis allows assigning tags to the data associated to a memory location and propagates those tags along the whole program. If two memory locations l and l' have the same tag then whenever data is stored in l it will be transferred to l'. Taint analysis is a special case of the Tag analysis where the analysis uses one tag representing "tainted" data.

The Tag analysis aims at being the "static" version of the Clang DataFlowSanitizer. Currently, the Tag analysis computes an over-approximation of the set of possible tags. Thus, the analysis cannot tell if a memory location is tagged with a particular tag, but instead, if it does not have a particular tag.

The Tag analysis is context-, field-, and flow-sensitive. All this sensitivity comes from the heap abstraction performed by sea-dsa, the Crab inter-procedural analysis and the Crab region abstract domain.

Declaring Tags

A tag is just a numeric identifier:

typedef uint64_t tag_t;

Add Tags

Tags are assigned to memory data by using a special function __CRAB_intrinsic_add_tag:

// Sets the tag for each address in [ptr,ptr+size) to the union of the
// current tag for that address and tag. 
// Assume that ptr is aligned and size is the word size.
extern void  __CRAB_intrinsic_add_tag(void *ptr, tag_t tag);

For instance, the following piece of code assigns the tag 1 to some memory data:

int x = 0;
__CRAB_intrinsic_add_tag(&x, 1);

Check Tags

Currently, we can only ask if some memory data does not have a particular tag. For that, we use the special C function __CRAB_intrinsic_check_does_not_have_tag:

// Check whether the data associated to ptr cannot have tag.
extern void  __CRAB_intrinsic_check_does_not_have_tag(void *ptr, tag_t tag);

Comming back to our example, we can check if the memory data pointed by &x does not have the tag 2:

__CRAB_intrinsic_check_does_not_have_tag(&x, 2);

Clam translates a call to __CRAB_intrinsic_check_does_not_have_tag into an assertion that holds if the data of &x does not have the tag 2. Therefore, the option --crab-check=assert should be always enabled when calls to __CRAB_intrinsic_check_does_not_have_tag are added into the program.

Options to run clam.py with the Tag analysis

--crab-inter
--crab-track=mem
--crab-heap-analysis=cs-sea-dsa
--crab-check=assert

For more information, check out the examples in the tests/tag-analysis directory.