Astrée: Standardkonformität

Astrée ist ein Werkzeug zur statischen Analyse von C-Quellcode, bei der das Haupt­augenmerk darauf liegt, Laufzeitfehler aufzudecken bzw. deren Abwesenheit zu beweisen. Dazu zählt z. B. jeder Gebrauch der Sprache, der nach den C99-, C11-, C17- und C18-Normen ein undefiniertes Verhalten aufweist.

Mit der neuesten Astrée-Version kann die Laufzeitfehleranalyse auch auf C++-Code angewendet werden, sowie auf gemischten C- und C++-Code. Unterstützt werden alle modernen Varianten der C++-Sprache, einschließlich C++17.

Darüberhinaus kann Astrées hochentwickelte Analyse-Engine dazu benutzt werden, den Quell­code auf verschiedenste sicherheits­relevante Eigenschaften hin zu überprüfen. Dazu zählt Konformität zu Standards wie CWE, SEI CERT und MISRA.

Diese Seite bietet einen Überblick darüber, welche Kriterien, Regeln und Empfehlungen dieser Standards Astrée überprüft.

C99

Im Anhang J von ISO/IEC 9899:1999 (E), ISO/IEC 9899:2011 und ISO/IEC 9899:2018 finden sich die Verhalten, die der jeweilige Standard als unspezi­fiziert, undefiniert oder implementierungs­abhängig erachtet. In drei Abschnitten werden dabei Hunderte von Szenarien behandelt.

Wie Astrée jedes einzelne dieser Szenarien abdeckt, ist in einem 34-seitigen PDF-Dokument beschrieben. Dieses finden Sie im Tool selbst unter „Help“ → „C compliance matrices“, oder erhalten es auf Anfrage kostenlos bei info@absint.com.

Vorschau des Dokuments zur C99-Konformität

Common Weakness Enumeration (CWE)

Die folgende Tabelle führt alle CWE-Regeln auf, die von Astrée 20.04 unterstützt werden. Dazu zählen Regeln mit der CWE-CCR-Abdeckung „Exact“, „CWE-more-abstract“ und „CWE-more-specific“. Zusätzlich sind Regeln mit der Abdeckung „CWE-partial“ grau dargestellt. Weitere Details können Sie im Astrée-Menü „Help“ finden, oder bei info@absint.com erfragen.

Astrée-Analysen sind sicher, d. h. jede Regel, die verletzt wird, wird auch als verletzt ge­meldet.

15External control of system or configuration setting
73External control of file system or path
77Improper neutralization of special elements used in a command (command injection)
78Improper neutralization of special elements used in an OS command (OS-command injection)
79Improper neutralization of input during Web page generation (cross-site scripting)
88Argument injection or modification
89Improper neutralization of special elements used in an SQL command (SQL injection)
90Improper neutralization of special elements used in an LDAP command (LDAP injection)
91XML injection (aka blind XPath injection)
99Improper control of resource identifiers (resource injection)
117Improper output neutralization for logs
118Improper access of indexable resource
119Improper restriction of operations within the bounds of a memory buffer
120Buffer copy without checking size of input (‘classic buffer overflow‘)
121Stack-based buffer overflow
122Heap-based buffer overflow
123Write-what-where condition
124Buffer underwrite
125Out-of-bounds read
126Buffer over-read
127Buffer under-read
128Wrap-around error
129Improper validation of array index
130Improper handling of length parameter inconsistency
131Incorrect calculation of buffer size
134Uncontrolled format string
170Improper null termination
188Reliance on data/memory layout
190Integer overflow or wraparound
191Integer underflow or wraparound
193Off-by-one error
194Unexpected sign extension
195Signed to unsigned conversion error
196Unsigned to signed conversion error
197Numeric truncation error
240Improper handling of inconsistent structural elements
242Use of inherently dangerous function
252Unchecked return value
253Incorrect check of function return value
328Reversible one-way hash
362Concurrent execution using shared resource
with improper synchronization (‘race condition’)
364Signal handler race condition
365Race condition in switch
366Race condition within a thread
367Time-of-check time-of-use (TOCTOU) race condition
369Divde by zero
398Indicator of poor code quality
401Improper release of memory before removing last reference (memory leak)
404Improper resource shutdown or release
411Resource locking problems
415Double free
416Use after free
456Missing initialization of a variable
457Use of uninitialized variable
466Return of pointer value outside of expected range
467Use of sizeof() on a pointer type
468Incorrect pointer scaling
471Modification of assumed-immutable data (MAID)
475Undefined behavior for input to API
476NULL pointer dereference
477Use of obsolete functions
478Missing default case in switch statement
481Assigning instead of comparing
497Exposure of system data to an unauthorized control sphere
558Use of getlogin() in multithreaded application
561Dead code
562Return of stack variable address
567Unsynchronized access to shared data in a multithreaded context
573Improper following of specification by caller
587Assignment of a fixed address to a pointer
588Attempt to access child of a nonstructure pointer
611Improper restriction of XML External Entity reference (XXE)
628Function call with incorrectly specified arguments
643Improper neutralization of data within XPath expressions (XPath injection)
662Improper synchronization
663Use of a non-reentrant function in a concurrent context
665Improper initialization
666Operation on resource in wrong phase of lifetime
667Improper locking
672Operation on a resource after expiration or release
676Use of potentially dangerous function
680Integer overflow to buffer overflow
681Incorrect conversion between numeric types
682Incorrect calculation
685Function call with incorrect number of arguments
686Function call with incorrect argument type
690Unchecked return value to NULL pointer dereference
704Incorrect type conversion or cast
754Improper check for unusual or exceptional conditions
759Use of a one-way hash without a salt
761Free of pointer not at start of buffer
763Release of invalid pointer or reference
764Multiple locks of a critical resource
765Multiple unlocks of a critical resource
767Access to critical private variable via public method
783Operator precedence logic error
785Use of path manipulation function without maximum-sized buffer
786Access of memory location before start of buffer
787Out-of-bounds write
789Uncontrolled memory allocation
805Buffer access with incorrect length value
806Buffer access using size of source buffer
807Reliance on untrusted inputs in a security decision
822Untrusted pointer dereference
823Use of out-of-range pointer offset
824Access of uninitialized pointer
825Expired pointer dereference
831Signal handler function associated with multiple signals
832Unlock of a resource that is not locked
833Deadlock
835Loop with unreachable exit condition (‘infinite loop’)
908Use of uninitialized resource

SEI CERT C/C++ Coding Standard

Die folgenden Tabellen listen die von Astrée 20.04 unterstützten SEI-CERT-Regeln und -Empfehlungen. Die aus­gegrauten Einträge werden nur teilweise unterstützt. Ausrufezeichen markieren Empfehlungen, die per Definition von keinem Tool automatisch überprüft werden können. Weitere Details erhalten Sie auf Anfrage bei info@absint.com.

Regel 01: Präprozessor
PRE30-C Do not create a universal character name through concatenation
PRE32-C Do not use preprocessor directives in invocations of function-like macros
Regel 02: Deklarationen und Initialisierung
DCL30-C Declare objects with appropriate storage durations
DCL31-C Declare identifiers before using them
DCL36-C Do not declare an identifier with conflicting linkage classifications
DCL37-C Do not declare or define a reserved identifier
DCL38-C Use the correct syntax when declaring a flexible array member
DCL40-C Do not create incompatible declarations of the same function or object
DCL41-C Do not declare variables inside a switch statement before the first case label
Regel 03: Ausdrücke
EXP30-C Do not depend on the order of evaluation for side effects
EXP32-C Do not access a volatile object through a nonvolatile reference
EXP33-C Do not read uninitialized memory
EXP34-C Do not dereference null pointers
EXP36-C Do not cast pointers into more strictly aligned pointer types
EXP37-C Call functions with the correct number and type of arguments
EXP40-C Do not modify constant objects
EXP42-C Do not compare padding data
EXP43-C Avoid undefined behavior when using restrict-qualified pointers
EXP44-C Do not rely on side effects in operands to sizeof, _Alignof, or _Generic
EXP45-C Do not perform assignments in selection statements
EXP46-C Do not use a bitwise operator with a Boolean-like operand
Regel 04: Integer
INT30-C Ensure that unsigned integer operations do not wrap
INT31-C Ensure that integer conversions do not result in lost or misinterpreted data
INT32-C Ensure that operations on signed integers do not result in overflow
INT33-C Ensure that division and remainder operations do not result in divide-by-zero errors
INT34-C Do not shift an expression by a negative number of bits
or by greater than or equal to the number of bits that exist in the operand
INT35-C Use correct integer precisions
INT36-C Converting a pointer to integer or integer to pointer
Regel 05: Gleitkommazahlen
FLP30-C Do not use floating-point variables as loop counters
FLP32-C Prevent or detect domain and range errors in math functions
FLP34-C Ensure that floating-point conversions are within range of the new type
FLP36-C Preserve precision when converting integral values to floating-point type
FLP37-C Do not use object representations to compare floating-point values
Regel 06: Felder
ARR30-C Do not form or use out-of-bounds pointers or array subscripts
ARR36-C Do not subtract or compare two pointers that do not refer to the same array
ARR37-C Do not add or subtract an integer to a pointer to a non-array object
ARR38-C Guarantee that library functions do not form invalid pointers
ARR39-C Do not add or subtract a scaled integer to a pointer
Regel 07: Zeichen und Strings
STR30-C Do not attempt to modify string literals
STR31-C Guarantee that storage for strings has sufficient space
for character data and the null terminator
STR32-C Do not pass a non-null-terminated character sequence
to a library function that expects a string
STR37-C Arguments to character-handling functions must be
representable as an unsigned char
STR38-C Do not confuse narrow and wide character strings and functions
Regel 08: Speicherverwaltung
MEM30-C Do not access freed memory
MEM31-C Free dynamically allocated memory when no longer needed
MEM33-C Allocate and copy structures containing a flexible array member dynamically
MEM34-C Only free memory allocated dynamically
MEM35-C Allocate sufficient memory for an object
MEM36-C Do not modify the alignment of objects by calling realloc()
Regel 09: Input/Output
FIO37-C Do not assume that fgets() or fgetws()
returns a nonempty string when successful
FIO38-C Do not copy a FILE object
FIO39-C Do not alternately input and output from a stream without an intervening flush or positioning call
FIO41-C Do not call getc(), putc(), getwc() or putwc() with a stream argument that has side effects
FIO42-C Close files when they are no longer needed
Regel 10: Umgebung
ENV30-C Do not modify the object referenced by the return value of certain functions
ENV33-C Do not call system()
Regel 11: Signale
SIG30-C Call only asynchronous-safe functions within signal handlers
SIG31-C Do not access shared objects in signal handlers
SIG34-C Do not call signal() from within interruptible signal handlers
Regel 12: Fehlerbehandlung
ERR30-C Set errno to zero before calling a library function known to set errno, and check errno only after the function returns a value indicating failure
ERR33-C Detect and handle standard library errors
Regel 14: Nebenläufigkeit
CON30-C Clean up thread-specific storage
CON31-C Do not destroy a mutex while it is locked
CON32-C Prevent data races when accessing bit-fields from multiple threads
CON33-C Avoid race conditions when using library functions
CON35-C Avoid deadlock by locking in a predefined order
CON37-C Do not call signal() in a multithreaded program
CON39-C Do not join or detach a thread that was previously joined or detached
CON40-C Do not refer to an atomic variable twice in an expression
Regel 48: Verschiedenes
MSC30-C Do not use the rand() function for generating pseudorandom numbers
MSC32-C Properly seed pseudorandom number generators
MSC33-C Do not pass invalid data to the asctime() function
MSC37-C Ensure that control never reaches the end of a non-void function
MSC38-C Do not treat a predefined identifier as an object if it might only be implemented as a macro
MSC40-C Do not violate constraints
Empfehlung 01: Präprozessor
PRE00-C Prefer inline or static functions to function-like macros
PRE01-C Use parentheses within macros around parameter names
PRE05-C Understand macro replacement when concatenating tokens
or performing stringification
!
PRE06-C Enclose header files in an inclusion guard
PRE07-C Avoid using repeated question marks
Empfehlung 02: Deklarationen und Initialisierung
DCL00-C Const-qualify immutable objects
DCL01-C Do not reuse variable names in subscopes
DCL07-C Include the appropriate type information in function declarators
DCL08-C Properly encode relationships in constant definitions !
DCL10-C Maintain the contract between the writer and caller of variadic functions
DCL11-C Understand the type issues associated with variadic functions !
DCL13-C Declare function parameters that are pointers to values not changed by the function as const
DCL15-C Declare file-scope objects or functions that do not need external linkage as static
DCL16-C Use L, not l, to indicate a long value
DCL17-C Beware of miscompiled volatile-qualified variables !
DCL18-C Do not begin integer constants with 0 when specifying a decimal value
DCL19-C Minimize the scope of variables and functions
DCL20-C Explicitly specify void when a function accepts no arguments
DCL21-C Understand the storage of compound literals !
DCL22-C Use volatile for data that cannot be cached !
DCL23-C Guarantee that mutually visible identifiers are unique
Empfehlung 03: Ausdrücke
EXP02-C Be aware of the short-circuit behavior of the logical AND and OR operators
EXP03-C Do not assume the size of a structure is the sum of the sizes of its members
EXP08-C Ensure pointer arithmetic is used correctly
EXP10-C Do not depend on the order of evaluation of subexpressions
or the order in which side effects take place
EXP12-C Do not ignore values returned by functions
EXP19-C Use braces for the body of an if, for, or while statement
EXP20-C Perform explicit tests to determine success, true and false, and equality
Empfehlung 04: Integer
INT00-C Understand the data model used by your implementation(s) !
INT02-C Understand integer conversion rules !
INT07-C Use only explicitly signed or unsigned char type for numeric values
INT08-C Verify that all integer values are in range
INT09-C Ensure enumeration constants map to unique values
INT12-C Do not make assumptions about the type of a plain int bit-field
when used in an expression
INT13-C Use bitwise operators only on unsigned operands
INT18-C Evaluate integer expressions in a larger size before comparing
or assigning to that size
Empfehlung 05: Gleitkommazahlen
FLP00-C Understand the limitations of floating-point numbers !
FLP01-C Take care in rearranging floating-point expressions !
FLP02-C Avoid using floating-point numbers when precise computation is needed
FLP03-C Detect and handle floating-point errors
FLP04-C Check floating-point inputs for exceptional values
FLP06-C Convert integers to floating point for floating-point operations
Empfehlung 06: Felder
ARR00-C Understand how arrays work !
ARR02-C Explicitly specify array bounds, even if implicitly defined by an initializer
Empfehlung 07: Zeichen und Strings
STR00-C Represent characters using an appropriate type
STR04-C Use plain char for characters in the basic character set
STR09-C Don’t assume numeric values for expressions with type plain character
STR11-C Do not specify the bound of a character array initialized with a string literal
Empfehlung 08: Speicherverwaltung
MEM01-C Store a new value in pointers immediately after free()
MEM04-C Beware of zero-length allocations
MEM07-C Ensure that the arguments to calloc(), when multiplied, do not wrap
Empfehlung 09: Input/Output
FIO14-C Understand the difference between text mode and binary mode with file streams !
Empfehlung 11: Signale
SIG01-C Understand implementation-specific details regarding signal handler persistence !
Empfehlung 12: Fehlerbehandlung
ERR06-C Understand the termination behavior of assert() and abort() !
Empfehlung 14: Nebenläufigkeit
CON00-C Avoid race conditions with multiple threads
CON01-C Acquire and release synchronization primitives in the same module,
at the same level of abstraction
CON03-C Ensure visibility when accessing shared variables
CON06-C Ensure that every mutex outlives the data it protects
Empfehlung 15: Nebenläufigkeit (POSIX)
CON00-C Avoid race conditions with multiple threads
Empfehlung 48: Verschiedenes
MSC01-C Strive for logical completeness
MSC04-C Use comments consistently and in a readable fashion
MSC07-C Detect and remove dead code
MSC12-C Detect and remove code that has no effect or is never executed
MSC13-C Detect and remove unused values
MSC15-C Do not depend on undefined behavior
MSC17-C Finish every set of statements associated with a case label
with a break statement
MSC20-C Do not use a switch statement to transfer control into a complex block
MSC23-C Beware of vendor-specific library and language differences
MSC24-C Do not use deprecated or obsolescent functions
Empfehlung 51: Microsoft Windows
WIN03-C Understand HANDLE inheritance !

MISRA C/C++

RuleChecker-Screenshot

Astrée unterstützt MISRA-C:2004, MISRA-C:2012 (inklusive die Zusätze 1 und 2) und MISRA-C++:2008. Die Checks sind fein kon­figurierbar. Jede Regel und sogar einzelne Aspekte bestimmter Regeln können individuell hinzu­geschaltet werden.

Das aktuelle Release überprüft insgesamt 474 Regeln der drei Regelsets. Eine dreißigseitige PDF-Beschreibung, wie Astrée jede einzelne Regel behandelt, ist auf Anfrage kostenlos erhältlich. Kontaktieren Sie dazu info@absint.com.

Nachfolgend ist nur ein schneller Überblick all der unterstützten Regelkategorien.

MISRA-C:2004
1Environment
2Language extensions
3Documentation
4Character sets
5Identifiers
6Types
7Constants
8Declarations and definitions
9Initialization
10Arithmetic type conversions
11Pointer type conversions
12Expressions
13Control statement expressions
14Control flow
15Switch statements
16Functions
17Pointers and arrays
18Structures and unions
19Preprocessing directives
20Standard libraries
21Run-time failures
MISRA-C:2012
DDirectives
1A standard C environment
2Unused code
3Comments
4Character sets and lexical convention
5Identifiers
6Types
7Literals and constants
8Declarations and definitions
9Initialization
10The essential type model
11Pointer type conversions
12Expressions
13Side effects
14Control statement expressions
15Control flow
16Switch statements
17Functions
18Pointers and arrays
19Overlapping storage
20Preprocessing directives
21Standard libraries
22Resources
MISRA-C:2012 Amendment 1
12Expressions
21Standard libraries
MISRA-C++:2008
Unterstützung für C++ ist seit dem neuesten Release 18.04 erhältlich. Die meisten MISRA-C++:2008-Regeln werden bereits unterstützt.

ISO/IEC TS 17961:2013

Die folgende Tabelle listet die von Astrée 16.10 unterstützten Regeln der ISO/IEC-TS-17961:2013-Norm. Die aus­gegrauten Einträge werden nur teilweise unterstützt. Weitere Details erhalten Sie auf Anfrage bei info@absint.com.

2Accessing freed memory
6Calling functions with incorrect arguments
10Converting a pointer to integer or integer to pointer
11Converting pointer values to more strictly aligned pointer types
12Copying a FILE object
13Declaring the same function or object in incompatible ways
14Dereferencing an out-of-domain pointer
15Escaping of the address of an automatic object
17Use of an implied default in a switch statement
21Allocating insufficient memory
22Forming or using out-of-bounds pointers or array subscripts
23Freeing memory multiple times
26Integer division errors
28Modifying string literals
29Modifying the string returned by getenv, localeconv, setlocale, and strerror
30Overflowing signed integers
34Reallocating or freeing memory that was not dynamically allocated
35Referencing uninitialized memory
36Subtracting or comparing two pointers that do not refer to the same array
38Taking the size of a pointer to determine the size of the pointed-to type
39Using a tainted value as an argument to an unprototyped function pointer
44Using identifiers that are reserved for the implementation
46Tainted, potentially mutilated, or out-of-domain integer values are used in a restricted sink