Tools

SafeProver - Model Checker

SafeProver is a formal verification tool that performs both reachability and invariant satisfaction analysis. It uses Bounded Model Checking (BMC) as a refutation technique for counterexample detection and a set of algorithms derived from the K-Induction principle for invariant satisfaction. The proof engine offers the possibility to formally analysis any dicrete-time and bounded system in an exhaustive manner.

safeprover

Carto-C - Cyber Security flaws detection in C code

  • Computes the software attack surface
  • Detects target CWEs
  • Identifies the detected CWEs exploitable from the attack surface

IFFree Static Code Analyzer for Freedom From Interference evaluation

Road vehicles - Functional Safety standard ISO 26262 (Part 1, Definition 1.49) defines Freedom From Interference (FFI) as the absence of cascading failures between two or more elements that could lead to the violation of a safety requirement. Element X interferes with Element Y if there exists a failure of Element X that causes Element Y to fail.

A system is Free From Interference, if the failure of any element in the system cannot lead to the failure of any another element. That is, any element is free from interference with respect to all other elements of the system.

Three interference domains are defined in (ISO 26262-6 Annex D): timing and execution, memory management, exchange of information.

Interference notion extension

This notion can be extended to any piece of software mixing elements of different (safety or security) levels (two or more) without developing all the elements in compliance with the highest level.

iffree
FFI at Source Code Level

Interferences have their origin in

  • A high level function :
    • Reading low level memory
    • Calling low level functions
  • A low level function :
    • Writing high level memory
    • Calling high level functions

IFFree tackles Memory Corruption

  • The memory declared by high level module is an asset
  • An high level function does not corrupt high level memory

IFFree computes all the Interferences

iffree

IFFree Locates the call protections to add to make the application Interference Safe

DataRace

The ISO 26262: Road vehicles - Functional Safety standard ISO 26262 requires in clause 7.4.14 that "mechanisms for error detection as listed in Table 4 shall be applied". In Table 4 "Detection of data errors" is required for all ASIL levels.

Moreover, clause 7.4.11 states that "it shall be insured that the shared resources are used in such a way that freedom from interference of software partitions is ensured".

General description

A DataRace between two tasks arises when the outcome of the computation of at least one tasks depends on the relative speeds of the tasks. A data race occurs when two instructions access the same memory location and at least one of these accesses is a write.

The Bernstein's equations define conditions for noninterfering computations and avoiding any data race condition. For task Tj, Wj (respectively Rj) denotes the set of global variables written (respectively read or referenced) during the execution of the task.

Two tasks Ti and Tj do not share variables iff: Ri ᴖWj = Ø & Rj ᴖWi = Ø & Wi ᴖWj = Ø.

A variable v is shared between Ti and Tj iff it belongs to one of the subset Ri ᴖWj, Rj ᴖWi or Wi ᴖWj.

Accessing shared variables needs careful control: only one process should access the resource at a time. Mutual exclusion zones are implemented to insure that this property is verified by the code. As a result, a shared variable v raises a data race iff at least one of it accesses is not protected.

datarace

    DataRace computes:
  • all accesses to global variables performed from each declared task.
  • the shared variables using the Bernstein conditions.
  • the shared variables that raise data races.

StackWalker Static Code Analyzer for memory stacks worst case computation

The ISO 26262: Road vehicles - Functional Safety standard ISO 26262 (Part 6, Clause 7.4.47) requires "An upper estimation of required resources for the embedded software shall be made, including: the execution time, the storage space (RAM for stack and heaps ...); and the communications resources".

In Table 13 - Methods for software integration testing, method "1d Resource usage test" specifies that "To ensure the fullfilment of requirements influenced by the hardware architectural design with sufficient totlerance, properties such as ... storage usage (RAM for stack and heaps ...) ... have to be determined."

General description

A stack is a last in first out (LIFO) data structure whose primary operations are push and pop. The call stack is divided into tow separate parts: the user stack stores the call procedure’s local data (actual arguments, local variables), the system stack stores the linking information that allow the procedure to return to its caller.

Each thread in a multi-tasking operating system maintains its own stack space.

Independently of the compiler, the user stack follows general rules: the push size is related to the object pushed size, the push address is related to the alignment requirement. To fit the push size and address some padding is added.

stackwalker

  • StackWalker computes the maximum stack usage of each entry point (task) over all call graph execution paths: divided into user and system stack usage.
  • StackWalker provides a compiler definition for the Tasking compiler that can be customized to declare elementary sizes for the customer compiler.
  • StackWalker allows the user to declare impossible execution path sections that STW must not follow during the maximum size computation.

Resume: StackWalker - DataRace - IFFree - Carto-C stackwalker datarace iffree cartoc