...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Science of Computer Programming >Formal verification of side-channel countermeasures using self-composition
【24h】

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 NaCI security policies in real-world cryptographic code, highlighting the potential for automation of our techniques.
机译：加密软件实现的形式验证对现成的工具提出了重大挑战。这是由于代码的特定于域的特性，包括积极的优化和非功能性的安全要求，即针对旁通道攻击的对策的关键方面。在本文中，我们扩展了先前的结果，这些结果支持无干扰的自组合证明的实用性及其推广。我们将对最近提议的NaCl密码库的实施中采用的高级安全策略进行形式验证。我们将这些策略形式化，并提出一种基于自我组成的正式验证方法，从而扩展了以前可以使用此技术处理的安全策略的范围。我们通过解决现实世界密码中对NaCI安全策略的合规性来证明我们的结果，并强调了技术自动化的潜力。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号