SafeRiver develops a static
tool devoted to the exploration of software security in order to
improve audit quality (reproducibility, coverage …). Automatic tools
based on abstract interpretation take into account all possible
executions and pointer aliasing and perform inter-procedural forward or
backward analysis whereas these features are out of reach for a human
auditor. Carto-C enables exhaustive reproducible security audits.
Carto-C computes (from the source code of the application) :
- The attack surface :
- The entry/exit points,
- The input/output channels,
- The calls to external libraries,
- The protections declared by the user,
- The precious data declared by the user.
- The vulnerabilities listed below:
- CWE-78: Improper Neutralization of Special Elements used in an OS Command ('OS Command Injection');
- CWE-121: Stack Based Buffer Overflow;
- CWE-122: Heap Based Buffer Overflow;
- CWE-124: Buffer Underwrite;
- CWE-125 : Out-of-bounds Read;
- CWE-126: Buffer Overread;
- CWE-127: Buffer Underread;
- CWE-134: Uncontrolled Format String;
- CWE-190 or CWE-191: Integer Overflow or Wraparound or Integer Underflow (Wrap or Wraparound) ;
- CWE-369 : Divide By Zero;
- CWE-398 : Indicator of Poor Code Quality;
- CWE-401 : Improper Release of Memory Before Removing Last Reference (Memory Leak);
- CWE-457: Use of Uninitialized Variable;
- CWE-476: NULL Pointer Dereference;
- CWE-587 : Out-of-bounds Write;
- CWE-588: Attempt to Access Child of Non Structure Pointer;
- CWE-590: Free Memory Not on Heap;
- CWE-628: Function Call with Incorrectly Specified Arguments;
- CWE-665 : Improper Initialization;
- CWE-681 : Incorrect Conversion between Numeric Types;
- CWE-685: Function Call With Incorrect Number of Arguments;
- CWE-688: Function Call With Incorrect Variable or Reference as Argument;
- CWE-749: Exposed Dangerous Method or Function (format and command execution function).
Carto-C has been evaluated on
the NIST SATE test
base Juliet 1.2
Juliet 1.2 :
- Is a suite of 45000 elementary test cases
- Contains test cases implementing flaws and indicate dangerous code points
- Contains test cases implementing fix and indicate non dangerous code points
- Pass all test cases except unsuported
- Detects all flaws identified in Juliet.
Carto-C supports :
- The C language;
- The standard libraries: libC and POSIX;
- Linux and Windows source codes.
Carto-C 1.3.4 does not support :
- Backward goto;
- Recursive functions;
- Variadic functions;
- Wide strings.
Faure home page.