ISO/IEC JTC 1/SC22/WG14 N1254
1 September 2007
Thomas Plum,
tplum@plumhall.com
Saturation in C1x
WG14 N1254: Saturation in C1x
Introduction
Within the safety and security communities,
there is an important need to determine that
certain computed results have not been contaminated
by integer overflow.
Languages that compete with C
have traditionally met that need using methods that are awkward
for C;
this category would include
the throwing of exceptions (or signals),
encoding ranges into the integer types, and
the use of arbitrary-precision (“BigInt”) libraries.
(Call this category the “awkward methods”.)
However, in C1x we could meet this need by providing
saturation semantics for overflow-handling.
Discussion
There has been discussion within both WG14
and the
SC22 Other Working Group on Vulnerabilities
[OWGV]
of the CERT Secure Coding Standards
(see
[CERT-SCS],
[N1209],
and
[N1255]
).
Rule INT08-A is easy to state, and challenging to automate:
“Integer operations must result in an integer value within the
range of the integer type (that is, the resulting value is
the same as the result produced by unlimited-range integers).”
(We need a good name for this property of an integer value.
Unfortunately,
“in-range” carries the connotation of arbitrary
range-qualification, as in Ada or Pascal.
For now, I'll call it the
“correctly-represented” property.)
In the C standard, integer overflow produces undefined behavior;
i.e., any behavior is permitted, and in particular, producing
a saturated “MAX” result is permitted.
There is currently no way of
requiring a saturated result.
If in C1x we defined a new standard pragma such as
_Pragma(STDC SAT),
then without impacting existing code we could provide
the necessary semantics.
The basic idea is to permit static analyzers to determine
that specific calculated values have the
“correctly-represented” property,
without burdening the programmer with
unnecessary runtime overhead or a
one-macro-per-arithmetic-operator ugliness.
The languages that provide the
“awkward methods” don't automatically provide fully-automated
proofs of safety or security properties,
and a 21st-century C language could compete quite well,
if it is adequately static-analyzable.
Clearly, the compiler could deliver saturation semantics
at a runtime cost that beats any user-programmed solution.
For some result types, the hardware may already provide
saturating operators, for minimal overhead.
For completeness, we probably would want a pragma for modwrap and
for
“default” as well;
I leave the details for future deliberations.
The important point is to provide some portable guaranteed
method to obtain saturation semantics.
REFERENCES
[OWGV]
ISO/IEC JTC 1/SC 22/OWG:Vulnerabilities
http://www.aitcnet.org/isai/
[CERT-SCS]
CERT Secure Coding Standards
http://www.securecoding.cert.org/
[N1209]
http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1209.pdf
[N1255]
http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1255.pdf