A Context-Sensitive Memory Model for Verification of C/C++ Programs

2017 ◽  
pp. 148-168 ◽  
Author(s):  
Arie Gurfinkel ◽  
Jorge A. Navas
Keyword(s):  
Memory Model ◽  
C Programs ◽  
Context Sensitive

scholarly journals SecRSL: security separation logic for C11 release-acquire concurrency

2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-26
Author(s):  
Pengbo Yan ◽  
Toby Murray
Keyword(s):  
Information Flow ◽  
Separation Logic ◽  
Constant Time ◽  
Memory Model ◽  
C Programs ◽  
Information Flow Security ◽  
Empirical Performance ◽  
Functional Correctness ◽  
Local Reasoning ◽  
High Level

We present Security Relaxed Separation Logic (SecRSL), a separation logic for proving information-flow security of C11 programs in the Release-Acquire fragment with relaxed accesses. SecRSL is the first security logic that (1) supports weak-memory reasoning about programs in a high-level language; (2) inherits separation logic’s virtues of compositional, local reasoning about (3) expressive security policies like value-dependent classification. SecRSL is also, to our knowledge, the first security logic developed over an axiomatic memory model. Thus we also present the first definitions of information-flow security for an axiomatic weak memory model, against which we prove SecRSL sound. SecRSL ensures that programs satisfy a constant-time security guarantee, while being free of undefined behaviour. We apply SecRSL to implement and verify the functional correctness and constant-time security of a range of concurrency primitives, including a spinlock module, a mixed-sensitivity mutex, and multiple synchronous channel implementations. Empirical performance evaluations of the latter demonstrate SecRSL’s power to support the development of secure and performant concurrent C programs.

Efficient context-sensitive pointer analysis for C programs

1995 ◽  
Vol 30 (6) ◽  
pp. 1-12 ◽  
Author(s):  
Robert P. Wilson ◽  
Monica S. Lam
Keyword(s):  
Pointer Analysis ◽  
C Programs ◽  
Context Sensitive

scholarly journals GenMC: A Model Checker for Weak Memory Models

2021 ◽  
pp. 427-440
Author(s):  
Michalis Kokologiannakis ◽  
Viktor Vafeiadis
Keyword(s):  
Programming Languages ◽  
Error Detection ◽  
State Of The Art ◽  
Memory Models ◽  
Memory Model ◽  
Model Checker ◽  
C Programs ◽  
System Calls ◽  
Detection Capabilities ◽  
Additional Memory

AbstractGenMC is an LLVM-based state-of-the-art stateless model checker for concurrent C/C++ programs. Its modular infrastructure allows it to support complex memory models, such as RC11 and IMM, and makes it easy to extend to support further axiomatic memory models.In this paper, we discuss the overall architecture of the tool and how it can be extended to support additional memory models, programming languages, and/or synchronization primitives. To demonstrate the point, we have extended the tool with support for the Linux kernel memory model (LKMM), synchronization barriers, POSIX I/O system calls, and better error detection capabilities.

scholarly journals Verified compilation of C programs with a nominal memory model

2022 ◽  
Vol 6 (POPL) ◽  
pp. 1-31
Author(s):  
Yuting Wang ◽  
Ling Zhang ◽  
Zhong Shao ◽  
Jérémie Koenig
Keyword(s):  
Global Memory ◽  
Memory Model ◽  
Global Constraints ◽  
Concurrent Programs ◽  
Intuitive Reasoning ◽  
Contextual Memory ◽  
Memory Space ◽  
C Programs ◽  
Block Based ◽  
Verification Techniques

Memory models play an important role in verified compilation of imperative programming languages. A representative one is the block-based memory model of CompCert---the state-of-the-art verified C compiler. Despite its success, the abstraction over memory space provided by CompCert's memory model is still primitive and inflexible. In essence, it uses a fixed representation for identifying memory blocks in a global memory space and uses a globally shared state for distinguishing between used and unused blocks. Therefore, any reasoning about memory must work uniformly for the global memory; it is impossible to individually reason about different sub-regions of memory (i.e., the stack and global definitions). This not only incurs unnecessary complexity in compiler verification, but also poses significant difficulty for supporting verified compilation of open or concurrent programs which need to work with contextual memory, as manifested in many previous extensions of CompCert. To remove the above limitations, we propose an enhancement to the block-based memory model based on nominal techniques; we call it the nominal memory model. By adopting the key concepts of nominal techniques such as atomic names and supports to model the memory space, we are able to 1) generalize the representation of memory blocks to any types satisfying the properties of atomic names and 2) remove the global constraints for managing memory blocks, enabling flexible memory structures for open and concurrent programs. To demonstrate the effectiveness of the nominal memory model, we develop a series of extensions of CompCert based on it. These extensions show that the nominal memory model 1) supports a general framework for verified compilation of C programs, 2) enables intuitive reasoning of compiler transformations on partial memory; and 3) enables modular reasoning about programs working with contextual memory. We also demonstrate that these extensions require limited changes to the original CompCert, making the verification techniques based on the nominal memory model easy to adopt.

Sign in / Sign up

Export Citation Format

Share Document