Information-flow control on ARM and POWER multicore processors

作     者：Smith, Graeme Coughlin, Nicholas Murray, Toby 

作者机构：Def Sci & Technol Grp Brisbane Qld Australia Univ Queensland Sch Informat Technol & Elect Engn Brisbane Qld Australia Univ Melbourne Sch Comp & Informat Syst Melbourne Vic Australia 

出 版 物：《FORMAL METHODS IN SYSTEM DESIGN》 (系统设计中的形式方法)

年 卷 期：2021年第58卷第1-2期

页      面：251-293页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：Australian Research Council [DP160102457] Defence Science and Technology Group, Australia 

主　　题：Information-flow security Weak memory models Non-blocking algorithms 

摘      要：Weak memory models implemented on modern multicore processors are known to affect the correctness of concurrent code. They can also affect whether or not the concurrent code 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 ARM and POWER multicore processors leads to vulnerabilities in such programs, and present a compositional, flow-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. The logic has been proved sound with respect to existing operational semantics using Isabelle/HOL, and implemented in an automatic symbolic execution tool.