A logic for secure memory access of abstract state machines

Theoretical Computer Science（2005）

引用 3|浏览0

暂无评分

摘要

We extend the logic for abstract state machines by a read predicate that allows to make precise statements about the accesses of locations of an ASM. The logic can be used to prove security properties of ASMs like that the machine does not read locations containing critical information or that all accesses of the machine to the abstract memory are permitted. The new read predicate is also useful for proving refinements of parallel ASMs to sequential C-like programs. The logic is complete for hierarchical ASMs and still sound for turbo ASMs. It is integrated in the ASMKeY theorem prover.

查看译文

关键词

secure memory access,new read predicate,abstract state machines,parallel ASMs,abstract state machine,logic,sequentialization of parallel asms,secure information flow,read predicate,abstract memory,access predicate,turbo ASMs,hierarchical ASMs,ASMKeY theorem prover,critical information,C-like program

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要