کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
9657877 690055 2005 23 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
A logic for secure memory access of abstract state machines
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
A logic for secure memory access of abstract state machines
چکیده انگلیسی
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.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 336, Issues 2–3, 26 May 2005, Pages 343-365
نویسندگان
, ,