0在巴黎高等师范学校准备0机器级软件安全的语义方法0由Georges-Axel JALOYAN完成2021年9月14日0巴黎数学科学中心第386号学术学位0计算机专业0评审委员会成员：0Xavier RIVAL Inria – École normale supérieure 评审委员会主席0Lorenzo CAVALLARO 伦敦大学学院 评阅人0Sylvain GUILLEY 巴黎高科电信学院 评阅人0Whit�eld DIFFIE 斯坦福大学 评审员0Konstantinos MARKANTONAKIS 伦敦大学皇家霍洛威学院评审员0Clémentine MAURICE 法国国家科学研究中心 评审员0Aymeric VINCENT 原子能和可替代能源委员会 博士导师0David NACCACHE 巴黎高等师范学校 导师0Hovav SHACHAM 德克萨斯大学奥斯汀分校 客座教授0摘要0计算机科学建立在许多层次的抽象之上，从硬件到算法或工作声明。在计算机安全的背景下，漏洞往往源于这些不同抽象层之间的差异。这种不一致可能导致网络攻击造成损失。为了解决这个问题，提供语义有助于形式化描述并弥合这些层次之间的差距。在这篇论文中，我们通过将各种语义表示与每个抽象层的关系连接起来，改进了方法和程序。我们简要介绍了从头开始构建汇编语言以及在二进制利用的背景下构建和使用的各种抽象的基本概念和术语。在第一部分中，我们利用更高级的语义构造来减少几种最新指令集架构上高级攻击的设计复杂性。我们以教程的方式呈现了三个例子，分别解决了越来越复杂的约束条件。具体来说，我们描述了一种方法，可以自动将任意程序转换为ARMv8-A和RISC-V上的字母数字shellcode，并提供了关于在RISC-V上进行返回导向编程攻击的可行性的第一次分析。在第二部分中，我们看到如何使用形式化方法来提高各种语言或构造的安全性和安全性，通过三个例子分别优化Hoare监视器的实现，这是一种众所周知的同步构造，防止在不妨碍演绎验证的情况下在命令式语言中产生有害的别名，或者将二进制代码抽象为紧凑表示，从而实现进一步的协议解同步分析。0i0iiiii0摘要0计算机科学建立在许多层次的抽象之上，从硬件到算法或工作声明。在计算机安全的背景下，漏洞往往源于这些不同抽象层之间的差异。这种不一致可能导致网络攻击造成损失。为了解决这个问题，提供语义有助于形式化描述并弥合这些层次之间的差距。在这篇论文中，我们通过将各种语义表示与每个抽象层的关系连接起来，改进了方法和程序。我们简要介绍了从头开始构建汇编语言以及在二进制利用的背景下构建和使用的各种抽象的基本概念和术语。在第一部分中，我们利用更高级的语义构造来减少几种最新指令集架构上高级攻击的设计复杂性。我们以教程的方式呈现了三个例子，分别解决了越来越复杂的约束条件。具体来说，我们描述了一种方法，可以自动将任意程序转换为ARMv8-A和RISC-V上的字母数字shellcode，并提供了关于在RISC-V上进行返回导向编程攻击的可行性的第一次分析。在第二部分中，我们看到如何使用形式化方法来提高各种语言或构造的安全性和安全性，通过三个例子分别优化Hoare监视器的实现，这是一种众所周知的同步构造，防止在不妨碍演绎验证的情况下在命令式语言中产生有害的别名，或者将二进制代码抽象为紧凑表示，从而实现进一步的协议解同步分析。ivv0前言0迄今为止，人们由于对手段的无知而无法实现他们的希望。随着这种无知的消失，他们越来越能够将自己的物质环境、社会环境和自身塑造成他们认为最好的形式。只要他明智，这种新的力量就是有益的；只要他愚蠢，它就完全相反。因此，如果科学文明要成为一种良好的文明，增加知识必须伴随着增加智慧。0伯特兰∙罗素，《科学的展望》，1931年0本论文旨在通过实际例子展示可以利用的技术，将形式方法和计算机安全更加紧密地结合起来，以改进或利用各种产品或平台。这四年的研究使我深信，计算机安全需要一种严谨和经验的方法，既要深入理解实现细节，又要把握底层的抽象思想。任何误解都可能导致漏洞。由于网络攻击可能造成不成比例的损害，计算机安全本质上是吹毛求疵者的游乐场。另一方面，形式方法与安全关系不大，历史上与安全只有松散的联系。最近的努力旨在汇集黑客和形式方法专家，使混合方法获得动力，2016年DARPA网络大挑战赛在DEF CON24上的例子是最具象征意义的。随着形式方法的成熟，最新的工具在可扩展性、易用性和多功能性方面得到了改进，这种发展很可能会继续下去。在开始这篇论文时，我曾认为形式方法只是计算机安全的对偶；前者适用于防御，后者擅长攻击。回过头来看，这种观点是错误的，因为两者都提供了攻击和防御机制。事实上，形式方法通过系统的、严谨的研究程序的含义和语义，弥合了程序和模型之间的差距。本文的每一章都通过扩展版本的同行评审文章的方式展示了这种方法的一个例子。vivii0致谢0在开始这篇论文之前，我不得不注意到有多少人参与其中。有多少教授，有多少家庭成员，有多少朋友，有多少偶然的相遇，有多少匿名人士分享他们的知识碎片，让我有机会在法国两个最负盛名的机构——巴黎高等师范学校和法国原子能与替代能源委员会军事应用部门——完成我的博士学位。能够在这样的环境中工作是一种机遇和特权。接下来的感谢表达了我对那些帮助我走到今天的主要人物和机构的感激之情。我肯定会忘记一些人，他们往往是匿名的，但他们使这篇论文得以完成；因此，我要向他们集体表示感谢。首先要感谢我的导师DavidNaccache，他从第一天起就完全信任我。这始于你的科学计算课程的实践，这种信任一直持续到今天。在论文开始时，你开玩笑地告诉我，三年的时间比一些夫妻的时间还长。你已经连续七年成为我的老师、学术导师和博士导师，与你一起工作的喜悦仍然存在。我要非常感谢你教给我的一切，你帮我避免麻烦的次数，以及团队内的良好工作氛围。这种氛围与场地有关；高师通过其地理位置、历史、员工、研究人员和学生提供了一个激发创造力的特殊环境。我找不到更好的地方来完成我的博士学位，感谢DavidPointcheval，计算机系主任，让我在他的办公室里工作。我非常感谢我的博士导师AymericVincent，他在这三年里给了我宝贵的知识和丰富的经验。关于如何最好地表示所研究的协议的自动机类型的无休止讨论使我明白，研究是一个长期的智力过程。viii0这只是第一步。回顾过去，我意识到在计算机知识和科学文化方面取得了很大进步；你是其中的主要推动者。同样，这也与环境密切相关，因为原子能和可替代能源委员会是科学卓越的最佳体现之一。布吕耶勒沙特尔站位于巴黎以东30公里处，拥有充足的资源和设施，为研究提供了良好的条件。当然，还有一些附加条件，使这个地方更加迷人：位于Hurepoix地区的壮丽风景，一家享有盛誉的企业餐厅，以及许多活动可以让人们了解站点的研究团队。在这方面，我找不到更好的地方，感谢PascalMalterre让我加入他的网络安全团队。我要感谢评委会：Lorenzo Cavallaro、SylvainGuilley、Konstantinos Markantonakis、Xavier Rival、ClémentineMaurice、Whitfield Diffie、Aymeric Vincent、David Naccache和HovavShacham。他们的反馈非常宝贵，他们在整个过程中的指导非常有价值。同样，我要感谢Mathieu Blanc、Colas Le Guernic和Jean-ChristopheFilliâtre成为我的论文监督委员会成员，通过他们的帮助和建议解决了所有行政问题。科学是集体的工作，我真的很感激我的合著者们教给我研究的各种技巧。特别感谢HadrienBarral、Claire Dross、Houda Ferradi、Rémi Géraud、Maroua Maalej、KonstantinosMarkantonakis、Keith Mayes、Yannick Moy、David Naccache、Raja NaeemAkram、Andrei Paskevich、Lee Pike、David Robin和CarltonShepherd。我有幸与ENS和CEA的两个杰出的计算机安全团队合作，并感谢他们在科学和非科学讨论方面的高产出和有趣的交流。法语中有句谚语说，锻造使人成为铁匠。我相信这对于研究也是如此。实习为我提供了与工业和学术界著名团队合作的宝贵经验。我要感谢我的导师、他们的团队和机构给予我机会：Alwyn E. Goodloe和NASA Langley ResearchCenter的安全关键航空电子系统分部，Lee Pike和Galois的SMACCMPilot团队，YannickMoy和AdaCore的SPARK团队，Konstantinos Markantonakis和Royal HollowayUniversity of London的智能购物车和物联网安全中心，以及Sean McLaughlin和AmazonWebServices的自动推理小组。我还要感谢那些让我热爱数学和计算机的教授们，他们每个人都为此做出了贡献。比如，从六年级到高中毕业，每周二和周四的数学俱乐部，EricVuillemey通过各种游戏和谜题（如战棋、智力游戏等）教授数学，展示了数学不仅仅是一项计算任务。还有法国IOI在假期期间组织的密集培训，MathiasHiron和他的教练们每天教授10小时的算法，为国际信息学奥林匹克竞赛做准备。还有在Stanislas预科班上，CélestinRakotoniaina在数学课、考试和古典音乐会之间轮流，以及Marie-ChristinePauzin、Anne Gérard和VincentDesportes等教学团队。我的ENS教师在这些感谢中占据了特殊的位置，首先是我的导师Jean Vuillemin和David Naccache，以及优秀的教授Serge Abiteboul、Alexandred'Aspremont、Jean-Daniel Boissonnat、Anne Bouillard、Albert Cohen、SylvainConchon、Juliusz Chroboczek、Carole Delporte、Jérôme Férêt、Jean-ChristopheFilliâtre、Rémi Géraud、Jean Goubault-Larrecq、Emmanuel Haucourt、Jean-PaulLaumond、Claude Marché、Claire Mathieu、Paul-André Melliès、AntoineMiné、Castucia Palamidessi、David Pointcheval、Jean Ponce、Marc Pouzet、XavierRival、Pierre Senellart、Nicolas Schabanel、Jacques Stern和WiesławZielonka。我还要感谢我的学生和给我教学机会的教授们：在Stanislas的MPSI课程中与Alain Camanès一起进行的Caml实践课程，与RémiGéraud一起进行的密码学和网络安全课程，与DavidNaccache一起进行的法国国家宪兵学院MBAsp课程，与SylvainGuilley一起进行的ENS数字系统导论课程，与Jean-ChristopheFilliâtre一起进行的编程和编译实践课程。同样，我要感谢高等科学与技术研究所和网络防御指挥部，让我有机会向广大观众普及我的一部分研究成果。最后，我要特别感谢我的家人和父母，在过去的26年里一直支持、鼓励和帮助我。没有你们，这一切都不可能。ixmathématiques à travers de nombreux jeux et énigmes (backgammon, cassetêtes, ...), montrant que les mathématiques ne sont pas qu’une corvée cal-culatoire.Comme les stages intensifs organisés par France IOI pendantles vacances scolaires, où Mathias Hiron et ses entraîneurs enseignent 10heures par jour une semaine durant l’algorithmique en vue de préparer auxolympiades internationales d’informatique. Ou encore en prépa à Stanis-las, avec Célestin Rakotoniaina qui alterne entre cours de maths, khôlleset concerts de musique classique et le reste de l’équipe pégagogique avecMarie-Christine Pauzin, Anne Gérard et Vincent Desportes.Mes enseignants à l’ENS ont une place toute particulière dans ces re-merciements, en commençant par mes tuteurs Jean Vuillemin et David Nac-cache, et les excellents professeurs Serge Abiteboul, Alexandre d’Aspremont,Jean-Daniel Boissonnat, Anne Bouillard, Albert Cohen, Sylvain Conchon,Juliusz Chroboczek, Carole Delporte, Jérôme Férêt, Jean-Christophe Fil-liâtre, Rémi Géraud, Jean Goubault-Larrecq, Emmanuel Haucourt, Jean-Paul Laumond, Claude Marché, Claire Mathieu, Paul-André Melliès, An-toine Miné,Castucia Palamidessi, David Pointcheval, Jean Ponce, MarcPouzet, Xavier Rival, Pierre Senellart, Nicolas Schabanel, Jacques Sternet Wiesław Zielonka.J’aimerais aussi remercier mes élèves ainsi que les professeurs qui m’ontdonné l’opportunité d’améliorer mes compétences en pédagogie en me con-fiant une charge d’enseignement : les travaux pratiques de Caml en MPSIà Stanislas avec Alain Camanès, les interventions en cryptographie ou ensécurité informatique à Centrale Paris avec Rémi Géraud, les interventionsau MBAsp de l’École des officiers de la Gendarmerie nationale avec DavidNaccache, les travaux dirigés de systèmes numériques à l’École normalesupérieure avec Sylvain Guilley, les travaux pratiques de programmation etde compilation à l’École polytechnique avec Jean-Christophe Filliâtre. Demême, je remercie l’Institut des hautes études pour la science et la technolo-gie et le commandement de la cyberdéfense pour m’avoir permis de présenteren vulgarisant une partie des mes travaux à des publics élargis.Enfin une pensée toute particulière va à ma famille et à mes parents quim’ont soutenu, encouragé et aidé durant déjà vingt-six années. Sans vous,rien de tout cela ne serait possible.xContentsForeword. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .vRemerciements / Acknowledgments . . . . . . . . . . . . . . . . . .viiAbbreviations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .xv1Introduction31.1Outline. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .31.2Terminology . . . . . . . . . . . . . . . . . . . . . . . . . . . .41.3Results and Contributions . . . . . . . . . . . . . . . . . . . .51.3.1Thesis Results. . . . . . . . . . . . . . . . . . . . . .51.3.2Personal Bibliography . . . . . . . . . . . . . . . . . .62Prolegomena92.1Assembly 101 . . . . . . . . . . . . . . . . . . . . . . . . . . .92.1.1Top-down approach. . . . . . . . . . . . . . . . . . .102.1.2Bottom-up approach . . . . . . . . . . . . . . . . . . .122.2Operating systems . . . . . . . . . . . . . . . . . . . . . . . .222.3Binary exploitation . . . . . . . . . . . . . . . . . . . . . . . .29ILeveraging the instruction set architecture for con-strained exploitation353Alphanumeric shellcoding on ARMv8-A373.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . .373.2Preliminaries. . . . . . . . . . . . . . . . . . . . . . . . . . .383.2.1Prior and related work . . . . . . . . . . . . . . . . . .403.2.2ARMv8-A AArch64. . . . . . . . . . . . . . . . . . .403.2.3Shellcodes and exploitation . . . . . . . . . . . . . . .413.3Building the instruction set . . . . . . . . . . . . . . . . . . .423.4High-level constructs . . . . . . . . . . . . . . . . . . . . . . .453.4.1Register operations . . . . . . . . . . . . . . . . . . . .453.4.2Bitwise operations . . . . . . . . . . . . . . . . . . . .473.4.3Load and store operations . . . . . . . . . . . . . . . .493.4.4Pointer arithmetic . . . . . . . . . . . . . . . . . . . .503.4.5Branch operations. . . . . . . . . . . . . . . . . . . .50xixiiCONTENTS3.5Fully Alphanumeric AArch64 . . . . . . . . . . . . . . . . . .513.5.1The Encoder. . . . . . . . . . . . . . . . . . . . . . .513.5.2The Decoder. . . . . . . . . . . . . . . . . . . . . . .513.5.3Payload Delivery . . . . . . . . . . . . . . . . . . . . .523.5.4Assembly and machine code . . . . . . . . . . . . . . .523.5.5Polymorphic shellcode . . . . . . . . . . . . . . . . . .543.6Experimental results . . . . . . . . . . . . . . . . . . . . . . .543.6.1QEMU. . . . . . . . . . . . . . . . . . . . . . . . . .553.6.2DragonBoard 410c . . . . . . . . . . . . . . . . . . . .553.FHello World Shellcode . . . . . . . . . . . . . . . . . . . . . .644Alphanumeric shellcoding on RISC-V654.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . .654.1.1Prior and related work . . . . . . . . . . . . . . . . . .664.1.2Our contribution . . . . . . . . . . . . . . . . . . . . .664.2RISC-V instruction set . . . . . . . . . . . . . . . . . . . . . .674.3Alphanumeric RISC-V . . . . . . . . . . . . . . . . . . . . . .684.3.1Data processing . . . . . . . . . . . . . . . . . . . . . .694.3.2Control-flow instruction . . . . . . . . . . . . . . . . .704.3.3Memory processing . . . . . . . . . . . . . . . . . . . .704.4High-level design . . . . . . . . . . . . . . . . . . . . . . . . .714.5Detailed construction . . . . . . . . . . . . . . . . . . . . . . .724.5.1Stage 1. . . . . . . . . . . . . . . . . . . . . . . . . .724.5.2Locating the shellcode and jump over the encodedpayload . . . . . . . . . . . . . . . . . . . . . . . . . .744.5.3Fixing the store pointer . . . . . . . . . . . . . . . . .744.5.4Unpacking stage 2 . . . . . . . . . . . . . . . . . . . .744.5.5Stage 2. . . . . . . . . . . . . . . . . . . . . . . . . .754.5.6Payload . . . . . . . . . . . . . . . . . . . . . . . . . .764.5.7Integration/Linking. . . . . . . . . . . . . . . . . . .774.5.8Shellcoding in /RV64IAC . . . . . . . . . . . . . . . . .774.5.9Shellcoding in ’RV64IDC . . . . . . . . . . . . . . . . .784.6Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . .794.6.1QEMU. . . . . . . . . . . . . . . . . . . . . . . . . .794.6.2HiFive Unleashed . . . . . . . . . . . . . . . . . . . . .8003.7 结论 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5603.B 字母数字连接 . . . . . . . . . . . . . . . . . . . . 5703.D 解码器源代码 . . . . . . . . . . . . . . . . . . . . . . 5903.E.1 负载多态性 . . . . . . . . . . . . . . . . . . 62CONTENTSxiii4.7Conclusion and future work . . . . . . . . . . . . . . . . . . .814.A Hello World Shellcodes . . . . . . . . . . . . . . . . . . . . . .824.A.1#RV64IC QEMU Hello World . . . . . . . . . . . . . .834.A.2/RV64IAC QEMU Hello World. . . . . . . . . . . . .834.A.3’RV64IDC QEMU Hello World. . . . . . . . . . . . .844.BSource code . . . . . . . . . . . . . . . . . . . . . . . . . . . .845Return-Oriented Programming on RISC-V855.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . .865.25.7Proposed Countermeasures. . . . . . . . . . . . . . . . . . .995.8Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . 1015.9Conclusion and Future Work. . . . . . . . . . . . . . . . . . 1035.A Source code and artifact . . . . . . . . . . . . . . . . . . . . . 103IIImproving the safety of programming languages usingformal methods1056Lock Optimization for Hoare Monitors1076.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1076.2Hoare monitors . . . . . . . . . . . . . . . . . . . . . . . . . . 1096.2.1Tower: Hoare monitors for real-time systems. . . . . 1096.2.2Tower toolchain . . . . . . . . . . . . . . . . . . . . . . 1126.3Petri net semantics for Tower . . . . . . . . . . . . . . . . . . 1136.3.1Petri nets . . . . . . . . . . . . . . . . . . . . . . . . . 1136.3.2Denotational semantics of Tower . . . . . . . . . . . . 1146.3.3Safety Properties . . . . . . . . . . . . . . . . . . . . . 1176.4Lock Refinement . . . . . . . . . . . . . . . . . . . . . . . . . 1186.4.1Lock Optimization . . . . . . . . . . . . . . . . . . . . 1186.4.2New semantics . . . . . . . . . . . . . . . . . . . . . . 1216.4.3Proofs of Safety . . . . . . . . . . . . . . . . . . . . . . 12205.2.1 返回导向编程 . . . . . . . . . . . . . 8705.3 威胁模型和攻击概述 . . . . . . . . . . . . . . . 8905.3.2 在被入侵的系统上创建一个（隐藏的）持久后门 . . . . . . . . . . . . . . .. . . . . . 9105.5 链接Gadgets . . . . . . . . . . . . . . . . . . . . . . 9505.6.1 Debian chroot on HiFive Unleashed . . . . . . . . . . . 97xivCONTENTS6.5Experimental Results . . . . . . . . . . . . . . . . . . . . . . . 1236.6Case-Study: The SMACCMPilot Autopilot. . . . . . . . . . 1256.6.1Autopilot Architecture . . . . . . . . . . . . . . . . . . 1256.6.2Optimizing SMACCMPilot . . . . . . . . . . . . . . . 1276.7Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . 1286.8Conclusion. . . . . . . . . . . . . . . . . . . . . . . . . . . . 1297Pointers in SPARK1317.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1317.2Informal Overview of Alias Analysis in SPARK . . . . . . . . 1337.3µSPARK Language . . . . . . . . . . . . . . . . . . . . . . . . 1367.4Alias Safety Rules. . . . . . . . . . . . . . . . . . . . . . . . 1387.5Implementation and Evaluation . . . . . . . . . . . . . . . . . 1457.6Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . 1487.7Future Work. . . . . . . . . . . . . . . . . . . . . . . . . . . 1497.8Conclusion. . . . . . . . . . . . . . . . . . . . . . . . . . . . 1508Static Protocol Analysis1518.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1518.2Formal model . . . . . . . . . . . . . . . . . . . . . . . . . . . 1528.2.1Lifting binary into graphs. . . . . . . . . . . . . . . . . 1538.48.58.6Implementation and evaluation . . . . . . . . . . . . . . . . . 1618.6.1Main idea . . . . . . . . . . . . . . . . . . . . . . . . . 1618.6.2Transition system extraction. . . . . . . . . . . . . . 1628.6.3Detecting
我的内容管理
展开
