Weak memory models implemented on modern multicore processors are known to affect the correctness of concurrent code. They can also affect whether or not it is secure. This is particularly the case in programs where the security levels of variables are value-dependent, i.e., depend on the values of other variables. In this paper, we illustrate how instruction reordering allowed by contemporary multicore processors leads to vulnerabilities in such programs, and present a compositional, timing-sensitive information-flow logic which can be used to detect such vulnerabilities. The logic allows step-local reasoning (one instruction at a time) about a thread’s security by tracking information about dependencies between instructions which guarantee their order of occurrence. Program security can then be established from individual thread security using rely/guarantee reasoning.
CITATION STYLE
Smith, G., Coughlin, N., & Murray, T. (2019). Value-dependent information-flow security on weak memory models. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11800 LNCS, pp. 539–555). Springer. https://doi.org/10.1007/978-3-030-30942-8_32
Mendeley helps you to discover research relevant for your work.