Hendrik Tews, Marcus Völp, and Tjark Weber. In Franck Cassez, Ralf Huuck, Gerwin Klein, and Bastian Schlich, editors, Proceedings Seventh Conference on Systems Software Verification (SSV), volume 102 of EPTCS, pages 73-87, 2012.
In recent projects on operating-system verification, C and C++ data types are often formalized using a semantics that does not fully specify the precise byte encoding of objects. It is well-known that such an underspecified data-type semantics can be used to detect certain kinds of type errors. In general, however, underspecified data-type semantics are unsound: they assign well-defined meaning to programs that have undefined behavior according to the C and C++ language standards. A precise characterization of the type-correctness properties that can be enforced with underspecified data-type semantics is still missing. In this paper, we identify strengths and weaknesses of underspecified data-type semantics for ensuring type safety of low-level systems code. We prove sufficient conditions to detect certain classes of type errors and, finally, identify a trade-off between the complexity of underspecified data-type semantics and their type-checking capabilities.
@inproceedings{tews12underspecified,
author = {Hendrik Tews and Marcus V{\"o}lp and Tjark Weber},
title = {On the Use of Underspecified Data-Type Semantics for Type Safety in Low-Level Code},
editor = {Franck Cassez and Ralf Huuck and Gerwin Klein and Bastian Schlich},
booktitle = {Proceedings Seventh Conference on Systems Software Verification (SSV)},
volume = {102},
series = {EPTCS},
pages = {73--87},
year = {2012},
url = {http://dx.doi.org/10.4204/EPTCS.102.8}
}