A sound abstract memory model for static analysis of C programs

2018 ◽  
Vol 16 (3) ◽  
pp. 255
Author(s):  
Yukun Dong
Keyword(s):  
Static Analysis ◽  
Memory Model ◽  
C Programs

scholarly journals Enhancing the Security of C/C++ Programs using Static Analysis

2016 ◽  
Vol 9 (44) ◽  
Author(s):  
Subburaj Ramasamy ◽  
Anuj Singh ◽  
Deepak Singal
Keyword(s):  
Static Analysis ◽  
C Programs

SharpChecker: Static analysis tool for C# programs

2017 ◽  
Vol 43 (4) ◽  
pp. 268-276 ◽  
Author(s):  
V. K. Koshelev ◽  
V. N. Ignatiev ◽  
A. I. Borzilov ◽  
A. A. Belevantsev
Keyword(s):  
Static Analysis ◽  
Analysis Tool ◽  
C Programs ◽  
Static Analysis Tool

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.

Sign in / Sign up

Export Citation Format

Share Document