多学科开放存取档案HAL中关于二进制级代码的符号化分析在加密实现中应用于微架构攻击的检测

73 浏览量更新于2023-12-03 收藏 16.1MB PDF 举报

身份认证购VIP最低享 7 折!

领优惠券(最高得80元）

0HAL编号：tel-036424180https://theses.hal.science/tel-03642418v20提交日期：2022年4月15日0HAL是一个多学科开放存取档案，用于存储和传播科学研究文档，无论这些文档是否已发布。这些文档可以来自法国或国外的教育和研究机构，也可以来自公共或私人研究中心。0HAL（开放式多学科开放存取档案）是一个用于存储和传播研究文档的多学科开放存取档案，这些文档可以是法国或国外的教育和研究机构、公共或私人研究中心发布的或未发布的科学研究文档。0用于安全性的符号化二进制级代码分析。应用于加密代码中的微架构时序攻击的检测0Lesly-Ann Daniel0引用此版本：0Lesly-Ann Daniel. Symbolic binary-level code analysis for security. Application to the detection of mi-croarchitectural timing attacks in cryptographic code. Cryptography and Security [cs.CR]. UniversitéCôte d’Azur, 2021. English. �NNT : 2021COAZ4092�. �tel-03642418v2� 0二进制级代码的符号化分析0为了安全0应用于微架构攻击的检测0在加密实现中0Lesly-Ann Daniel0CEA List，INRIA INDES团队0为了获得蔚蓝海岸大学计算机科学博士学位，由Tamara Rezk指导，InriaINDES团队主任，SébastienBardin共同指导，CEAList高级研究员，于2021年11月12日答辩0评审委员会成员：Gilles Barthe，科学主任，MaxPlanck研究所 Cristian Cadar，教授，伦敦帝国学院Aurélien Francillon，副教授，EURECOM RobertoGuanciale，助理教授，瑞典皇家理工学院 BorisKöpf，研究员，微软剑桥研究院0博士学位论文0蔚蓝海岸大学科学与技术学院0信息与通信科学与技术0博士论文0为了获得以下学位0法国蔚蓝海岸大学计算机科学博士学位0Lesly-AnnDaniel提交并答辩0用于安全性的符号化二进制级代码分析0应用于加密代码中的微架构时序攻击的检测0论文导师：Tamara Rezk0在CEA List准备02021年11月12日答辩0导师：Tamara Rezk，Inria INDES团队主任，共同导师：Sébastien Bardin，CEAList高级研究员0评审委员会：0评阅人：Gilles Barthe，科学主任，Max Planck研究所 CristianCadar，教授，伦敦帝国学院评审人：Aurélien Francillon，副教授，EURECOMRoberto Guanciale，助理教授，瑞典皇家理工学院 BorisKöpf，研究员，微软剑桥研究院0i0蔚蓝海岸大学0摘要0用于安全性的符号化二进制级代码分析0计算机软件经常处理机密数据，通常使用加密程序来保证其机密性。在这种情况下，确保这些加密程序不能被攻击者利用来提取机密数据至关重要。不幸的是，即使加密算法基于坚实的数学基础，它们在物理世界中的执行会产生攻击者可以利用的副作用。特别是，攻击者可以利用程序的执行时间来推断有关其机密输入的信息，或者利用微架构中编码的机密数据进行攻击。最近，Spectre攻击表明，还可以利用处理器的优化（特别是推测机制）来提取机密数据。在这篇论文中，我们开发了自动程序分析工具，用于验证加密软件中机密数据的保密性。特别是，我们针对加密程序的三个关键属性进行了定位：（1）秘密擦除，确保机密数据在程序结束时从内存中擦除；（2）常量时间，保护免受微架构攻击；（3）推测常量时间，保护免受Spectre攻击。这些属性共同具有两个特点，使得它们难以分析。首先，它们是执行对的属性（即2-超安全性），这使它们与常规验证工具不兼容（设计用于安全性）。其次，它们通常不被编译器保留。在这篇论文中，我们的目标是设计自动符号化分析工具，对执行对进行建模，以二进制代码为基础，包括处理器的推测机制，并在现有的加密软件上进行扩展。我们的分析基于关系符号执行（一种符号执行对2-超安全性的适应），并通过优化来使其在二进制级别上高效，并有效地对程序的推测语义进行建模。我们提供了两个开源工具：Binsec/Rel，用于漏洞查找和有界的常量时间和秘密擦除验证；以及Binsec/Haunted，用于检测Spectre攻击的漏洞。我们的实验评估表明，与之前的方法相比，我们的优化显著提高了性能：减少了分析时间，发现了更多的漏洞，并使之前无法实现的加密原语的验证成为可能。我们使用我们的工具对各种加密原语和开源库的实用函数进行了分析（例如Libsodium、OpenSSL、BearSSL和HACL*），包括常量时间（338个二进制文件）、秘密擦除（680个二进制文件）和Spectre（45个二进制文件）。在这些工作中，我们发现了一些新的漏洞，以及一些软件保护措施的弱点。0关键词：二进制分析，形式方法，软件验证，符号执行，恒定时间，秘密擦除，Spectre。0ii0iii0尼斯大学0摘要0用于安全性的符号二进制级代码分析0程序通常执行涉及秘密数据的计算，依赖于加密代码来保证其机密性。在这种情况下，确保加密代码不能被攻击者利用以泄露秘密数据至关重要。不幸的是，即使加密算法基于安全的数学基础，它们在物理世界中的执行可能会产生可以被利用以恢复秘密的副作用。特别是，攻击者可以利用程序的执行时间来泄露秘密数据，或者使用计时来利用微架构中编码的秘密使用微架构计时攻击。最近，Spectre攻击表明，还可以利用处理器优化（特别是推测机制）来泄露秘密数据。在本论文中，我们开发了用于检查加密代码中秘密数据机密性的自动化程序分析。特别是，我们针对加密实现的三个关键属性进行目标分析：（1）秘密擦除，确保秘密数据在程序结束时从内存中擦除；（2）恒定时间，防止微架构计时攻击；（3）推测恒定时间，防止Spectre攻击。这些属性具有两个共同的特点，使它们具有挑战性的分析。首先，它们是跟踪对的属性（即2-超安全性），这使它们与标准验证框架（设计用于安全属性）不兼容。其次，它们并不总是由编译器保留。我们在本论文中的目标是设计用于二进制级别的跟踪对的自动符号分析，包括处理器推测，并且可以扩展到现实世界的加密代码。我们的分析建立在关系符号执行的基础上，即符号执行对2-超安全性的适应，我们通过专门的优化进行补充：（1）用于二进制级别高效的关系符号执行，（2）用于高效建模程序推测语义。我们将我们的分析实现为两个开源工具：Binsec/Rel，用于常量时间和秘密擦除的错误查找和有界验证；以及Binsec/Haunted，用于检测Spectre攻击的漏洞。我们的实验评估表明，我们的优化大大提高了性能，比之前的方法更快地进行分析，发现更多的错误，并在现实世界的加密原语上实现了有界验证，而之前的方法则超时。使用我们的工具，我们分析了一系列来自开源库（包括Libsodium、OpenSSL、BearSSL和HACL*）的加密原语和实用函数，用于常量时间（338个二进制文件）、秘密擦除（680个二进制文件）和Spectre（45个二进制文件）。在这个过程中，我们发现了一些新的错误，以及标准保护方案的弱点。0关键词：二进制分析，形式方法，软件验证，符号执行，恒定时间，秘密擦除，Spectre。Je suis inﬁniment reconnaissante pour toutes les personnes exceptionnelles que j’airencontrées pendant ces trois ans et pour tous les moments passés ensemble. Je citeen vrac : les animateurs de lsl-misc, les randonnées de la Bühler voyage company,Eugénie pour les après-midis guitare et les randonnées, les coureurs du LSL, toutela fabuleuse team Mississippi, la pause café dissidente et ses intenses discussions, lesnombreuses discussions Matrix, les amis de Morzine, les amis de PSL, les soirées jeux,les soirées tout court. Merci aussi à tous ceux que je n’ai pas cités mais qui m’ontaccompagné pendant ces trois ans.Je remercie Clément, Romain et Simon qui sont venus de loin pour assister à masoutenance. Je remercie aussi ma mère, mon père, ma soeur pour avoir toujours cruen moi. Enﬁn, mes plus profonds remerciements sont pour Olivier. Merci pour tapatience, pour ton support inconditionnel, et pour m’avoir suivie dans toutes mesfolles aventures.0v0致谢0首先，我要感谢我的导师Sébastien和Tamara。谢谢你们对我的信任和鼓励，让我尝试雄心勃勃的事情。谢谢你们宝贵的建议和仔细的校对，这对我进步和改进我的工作非常有帮助。我很享受与你们一起工作的这三年。我真诚地感谢Gilles Barthe、CristianCadar、Aurélien Francillon、Roberto Guanciale和BorisKöpf同意成为我的评委，特别是Gilles Barthe和CristianCadar对我的论文进行审查。我还要感谢FrankPiessens邀请我参与一个激动人心的项目，并接受我作为他团队的博士后。我感谢Inria的INDES团队的成员，在我写论文时欢迎我加入，这使我的写作经历更加愉快。我还要感谢ChristopherHauser在南加州大学的团队欢迎我。我感谢CEA，特别是LSL，为提供如此好的工作环境。谢谢所有的同事，你们是我所期望的最好的同事！我非常享受与你们在一起的时间，包括咖啡休息时间、下班后的啤酒、野餐、所有的伟大讨论等等。特别感谢所有的博士同学，感谢你们提供的支持。我很高兴能与你们分享这个经历。我也很高兴有机会向更广泛的观众展示我的工作，一次是与Florent和我们的PSES梦之队，一次是与Myriam；我感谢所有帮助我们改进演示的同事们。我也感谢在学术界旅程中遇到的许多人，他们让我了解了新的文化，在我远离家乡时让我感到被包容，特别是Sander和Sima。viiContentsRésuméiAbstractiiiAcknowledgementsvIIntroduction11Introduction31.1Context . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .31.2Goal and challenges. . . . . . . . . . . . . . . . . . . . . . . . . . . . .61.2.1Binary analysis for 2-hypersafety . . . . . . . . . . . . . . . . .61.2.2Reasoning about microarchitectural security . . . . . . . . . . .71.3Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .81.3.1Primary contributions overview . . . . . . . . . . . . . . . . . .81.3.2Secondary contributions . . . . . . . . . . . . . . . . . . . . . .91.4Outline. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .10IIBackground132Automated Program Analysis152.1Overview of program analysis . . . . . . . . . . . . . . . . . . . . . . .152.1.1Analysis by over-approximation . . . . . . . . . . . . . . . . . .162.1.2Analysis by under-approximation . . . . . . . . . . . . . . . . .172.2Symbolic execution . . . . . . . . . . . . . . . . . . . . . . . . . . . . .182.2.1Overview of symbolic execution . . . . . . . . . . . . . . . . . .182.2.2Bug-ﬁnding and bounded-veriﬁcation . . . . . . . . . . . . . . .192.2.3Limitations . . . . . . . . . . . . . . . . . . . . . . . . . . . . .202.3Binary analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .212.3.1What you see is not what you execute . . . . . . . . . . . . . .212.3.2Challenges of binary analysis. . . . . . . . . . . . . . . . . . .222.3.3Binsec: a binary-analysis platform . . . . . . . . . . . . . . . .242.3.3.1Features . . . . . . . . . . . . . . . . . . . . . . . . . .242.3.3.2Limitations . . . . . . . . . . . . . . . . . . . . . . . .242.3.4Semantics of a low-level language (DBA) . . . . . . . . . . . . .252.3.5Binary-level symbolic execution . . . . . . . . . . . . . . . . . .273Low-level Security333.1Information ﬂow properties. . . . . . . . . . . . . . . . . . . . . . . .333.1.1Deﬁnition of information ﬂow and noninterference. . . . . . .333.1.2Noninterference is a 2-hypersafety property. . . . . . . . . . .353.1.3Veriﬁcation of information ﬂow properties . . . . . . . . . . . .36viii3.2Timing and microarchitectural attacks . . . . . . . . . . . . . . . . . .373.2.1Timing attacks . . . . . . . . . . . . . . . . . . . . . . . . . . .373.2.2Cache attacks . . . . . . . . . . . . . . . . . . . . . . . . . . . .393.2.3Other microarchitectural side-channels . . . . . . . . . . . . . .403.2.4Constant-time . . . . . . . . . . . . . . . . . . . . . . . . . . . .413.3Transient execution attacks. . . . . . . . . . . . . . . . . . . . . . . .423.3.1Overview of transient execution attacks. . . . . . . . . . . . .423.3.2Spectre-PHT . . . . . . . . . . . . . . . . . . . . . . . . . . . .433.3.3Spectre-STL . . . . . . . . . . . . . . . . . . . . . . . . . . . . .443.3.4Mitigations . . . . . . . . . . . . . . . . . . . . . . . . . . . . .463.3.5Speculative constant-time . . . . . . . . . . . . . . . . . . . . .48IIIContributions514Binsec/Rel: Symbolic Binary Analyzer for Constant-Time534.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .534.2Motivating example. . . . . . . . . . . . . . . . . . . . . . . . . . . .564.2.1Constant-time analysis of a toy program . . . . . . . . . . . . .574.2.2Symbolic execution and self-composition . . . . . . . . . . . . .574.2.3Relational symbolic execution . . . . . . . . . . . . . . . . . . .584.2.4Challenge of binary-level analysis . . . . . . . . . . . . . . . . .594.3Concrete semantics and leakage model . . . . . . . . . . . . . . . . . .604.3.1Leakage model. . . . . . . . . . . . . . . . . . . . . . . . . . .604.3.2Secure program . . . . . . . . . . . . . . . . . . . . . . . . . . .604.4Binary-level relational symbolic execution . . . . . . . . . . . . . . . .614.4.1Binary-level RelSE for constant-time . . . . . . . . . . . . . . .624.4.1.1Security evaluation . . . . . . . . . . . . . . . . . . . .634.4.1.2Symbolic conﬁguration. . . . . . . . . . . . . . . . .634.4.1.3Symbolic evaluation . . . . . . . . . . . . . . . . . . .634.4.1.4Speciﬁcation of high and low input . . . . . . . . . . .664.4.1.5Bug-ﬁnding . . . . . . . . . . . . . . . . . . . . . . . .664.4.2.1On-the-ﬂy read-over-write . . . . . . . . . . . . . . . .664.4.2.3Fault-packing . . . . . . . . . . . . . . . . . . . . . . .694.4.3.1Correctness of RelSE. . . . . . . . . . . . . . . . . .714.4.3.3Relative completeness of RelSE . . . . . . . . . . . . .724.5Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .734.6.1Research questions and methodology . . . . . . . . . . . . . . .744.6.2.1Bounded-veriﬁcation . . . . . . . . . . . . . . . . . . .754.6.2.2Bug-Finding. . . . . . . . . . . . . . . . . . . . . . .764.6.2.3Preservation of constant-time by compilers. . . . . .784.6.3Comparison with standard techniques. . . . . . . . . . . . . .794.6.3.1Comparison with self-composition and RelSE . . . . .804.6.3.2Performance of simpliﬁcations. . . . . . . . . . . . .8004.4.2 用于二进制级别的RelSE优化 . . . . . . . . . . . . . . . 6604.4.2.2 清除污染 . . . . . . . . . . . . . . . . . . . . . . . . 6804.4.3 定理 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6904.4.3.2 正确的漏洞发现 . . . . . . . . . . . . . . . . . . . 7104.4.3.4 正确的有界验证 . . . . . . . . . . . . . . . 7204.6 实验评估 . . . . . . . . . . . . . . . . . . . . . . . . . . 7404.6.2 Binsec/Rel的有效性 . . . . . . . . . . . . . . . . . . . 75ix4.6.3.3Comparison against standard symbolic-execution . . .814.7Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .824.8Related work. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .834.9Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .855Generalization of Binsec/Rel and Application to Secret-Erasure875.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .875.2Motivating example. . . . . . . . . . . . . . . . . . . . . . . . . . . .895.3Concrete semantics and leakage model . . . . . . . . . . . . . . . . . .905.3.1Leakage model. . . . . . . . . . . . . . . . . . . . . . . . . . .905.3.2Secure program . . . . . . . . . . . . . . . . . . . . . . . . . . .935.4Parameterized relational symbolic execution . . . . . . . . . . . . . . .955.4.1Parameterized symbolic evaluation . . . . . . . . . . . . . . . .955.4.2Instantiation of leakage predicates. . . . . . . . . . . . . . . .975.4.3Adapting theorems and proofs for other leakage models. . . . 1005.5Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1015.6Application: compiler preservation of secret-erasure . . . . . . . . . . . 1015.6.1Naive implementations . . . . . . . . . . . . . . . . . . . . . . . 1025.6.2Volatile function pointer . . . . . . . . . . . . . . . . . . . . . . 1025.6.3Volatile data pointer . . . . . . . . . . . . . . . . . . . . . . . . 1035.6.4Memory barriers . . . . . . . . . . . . . . . . . . . . . . . . . . 1045.6.5Weak symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1055.6.6Oﬀ-the-shelf implementations . . . . . . . . . . . . . . . . . . . 1055.7Related work. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1065.8Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1076Binsec/Haunted: Symbolic Analyzer for Spectre1096.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1096.2Haunted RelSE in a nutshell . . . . . . . . . . . . . . . . . . . . . . . . 1126.2.1Binary-level RelSE in a nutshell . . . . . . . . . . . . . . . . . . 1136.2.2.2Haunted RelSE for Spectre-PHT . . . . . . . . . . . . 1156.2.3.2Haunted RelSE for Spectre-STL. . . . . . . . . . . . 1176.3.1Symbolic evaluation of expressions . . . . . . . . . . . . . . . . 1186.3.2.2Evaluation of conditional instructions . . . . . . . . . 1216.3.2.3Invalidate transient paths . . . . . . . . . . . . . . . . 1216.3.3Haunted RelSE for Spectre-STL. . . . . . . . . . . . . . . . . 1226.3.3.1Symbolic memory. . . . . . . . . . . . . . . . . . . . 1226.3.3.2Evaluation of load expressions. . . . . . . . . . . . . 1236.3.3.3Invalidate transient loads . . . . . . . . . . . . . . . . 1256.3.4Symbolic evaluation of instructions . . . . . . . . . . . . . . . . 1256.3.5Theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1286.4Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1286.5Experimental evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . 1296.5.1Research questions and methodology . . . . . . . . . . . . . . . 12906.2.2 Spectre-PHT . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113 6.2.2.1Spectre-PHT的显式恶魔化符号执行 . . . . . . . . . . . 11306.2.3 Spectre-STL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116 6.2.3.1Spectre-STL的显式恶魔化符号执行 . . . . . . . . . . . . 11606.3 Haunted RelSE的形式化 . . . . . . . . . . . . . . . . . . . . . 11806.3.2 Spectre-PHT的恶魔化符号执行 . . . . . . . . . . . . . . . . . . 120 6.3.2.1动态推测深度 . . . . . . . . . . . . . . . 121x6.5.2Performance for Spectre-PHT . . . . . . . . . . . . . . . . . . . 1306.5.3Performance for Spectre-STL . . . . . . . . . . . . . . . . . . . 1326.5.4Comparison with Pitchfork and KLEESpectre . . . . . . . . . . 1336.6New vulnerabilities and mitigations . . . . . . . . . . . . . . . . . . . . 1356.6.1Index-masking defense . . . . . . . . . . . . . . . . . . . . . . . 1366.6.2Position-independent code . . . . . . . . . . . . . . . . . . . . . 1376.6.3Stack protectors and stale returns . . . . . . . . . . . . . . . . . 1386.7Related work. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1386.8Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141IVConclusion and Future Work1437Conclusion and Future Work1457.1Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1457.2Perspectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 146Bibliography149A Proofs167A.1 Proofs of Chapter 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167A.1.1Proof of Lemma 1. . . . . . . . . . . . . . . . . . . . . . . . . 167A.1.2Proof of Lemma 2. . . . . . . . . . . . . . . . . . . . . . . . . 168A.1.3Proof of

下载后可阅读完整内容，剩余1页未读，立即下载