کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
435131 1441702 2013 17 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Formal verification of side-channel countermeasures using self-composition
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Formal verification of side-channel countermeasures using self-composition
چکیده انگلیسی

Formal verification of cryptographic software implementations poses significant challenges for off-the-shelf tools. This is due to the domain-specific characteristics of the code, involving aggressive optimizations and non-functional security requirements, namely the critical aspect of countermeasures against side-channel attacks. In this paper, we extend previous results supporting the practicality of self-composition proofs of non-interference and generalizations thereof. We tackle the formal verification of high-level security policies adopted in the implementation of the recently proposed NaCl cryptographic library. We formalize these policies and propose a formal verification approach based on self-composition, extending the range of security policies that could previously be handled using this technique. We demonstrate our results by addressing compliance with the NaCl security policies in real-world cryptographic code, highlighting the potential for automation of our techniques.


► We address compliance with side-channel security policies in the NaCl cryptographic library.
► We formalize these policies under a non-interference security formulation.
► We propose verifying security using program transformation and self-composition.
► We prove that our technique is sound and demonstrate it in off-the-shelf tools.
► We extend the range of side-channel countermeasures addressed by prior work.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 78, Issue 7, 1 July 2013, Pages 796–812
نویسندگان
, , , ,