کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
418044 681604 2015 24 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Fully abstract trace semantics for protected module architectures
ترجمه فارسی عنوان
معانی ریاضی کاملا انتزاعی برای معماری های ماژول محافظت شده
کلمات کلیدی
معانی کاملا انتزاعی، معانی ردیابی، زبان مونتاژ نشده معماری حفاظت شده ماژول ها، زبان رسمی
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
چکیده انگلیسی


• Formalises A+IA+I: an assembly language extended with protected module architectures – an isolation mechanism found in emerging processors.
• Presents two trace semantics for A+IA+I programs and proves that both are fully abstract w.r.t. the operational semantics.
• Details which problems arise when considering readout and writeout labels in the trace semantics of A+IA+I programs.

Protected module architectures (PMAs) are isolation mechanisms of emerging processors that provide security building blocks for modern software systems. Reasoning about these building blocks means reasoning about elaborate assembly code, which can be very complex due to the loose structure of the code. One way to overcome this complexity is providing the code with a well-structured semantics. This paper presents one such semantics, namely a fully abstract trace semantics, for an assembly language enhanced with PMA. The trace semantics represents the behaviour of protected assembly code with simple abstractions, unburdened by low-level details, at the maximum degree of precision. Furthermore, it captures the capabilities of attackers to protected code and simplifies the formulation of a secure compiler targeting PMA-enhanced assembly language.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Computer Languages, Systems & Structures - Volume 42, July 2015, Pages 22–45
نویسندگان
, ,