A Scalable Memory Model for Low-Level Code

摘要

Because of its critical importance underlying all other software, low-level system software is among the most important targets for formal verification.Low-level systems software must sometimes make type-unsafe memory accesses,but because of the vast size of available heap memory in today's computer sys-tems, faithfully representing each memory allocation and access does not scalewhen analyzing large programs. Instead, verification tools rely on abstract mem-ory models to represent the program heap. This paper reports on two related in-vestigations to develop an accurate (i.e., providing a useful level of soundnessand precision) and scalable memory model: First, we compare a recently intro-duced memory model, specifically designed to more accurately model low-levelmemory accesses in systems code, to an older, widely adopted memory model.Unfortunately, we find that the newer memory model scales poorly compared tothe earlier, less accurate model. Next, we investigate how to improve the sound-ness of the less accurate model. A direct approach is to add assertions to the codethat each memory access does not break the assumptions of the memory model,but this causes verification complexity to blow-up. Instead, we develop a novel,extremely lightweight static analysis that quickly and conservatively guaranteesthat most memory accesses safely respect the assumptions of the memory model,thereby eliminating almost all of these extra type-checking assertions. Further-more, this analysis allows us to create automatically memory models that flexiblyuse the more scalable memory model for most of memory, but resorting to a moreaccurate model for memory accesses that might need it.