On the Use of Underspecified Data-Type Semantics for Type Safety in Low-Level Code

TL;DR

This paper investigates the use of underspecified data-type semantics in low-level code to detect type errors, analyzing their strengths, limitations, and the trade-offs involved in ensuring type safety.

Contribution

It provides a formal analysis of underspecified data-type semantics, identifying conditions for detecting type errors and discussing the balance between semantic complexity and type-checking power.

Findings

Underspecified semantics can detect certain type errors in low-level code.

There are inherent limitations and unsoundness in using underspecified semantics for type safety.

A trade-off exists between the complexity of semantics and their effectiveness in error detection.

Abstract

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.