注释语义的非局部分析认证：数学与信息与通信科学与技术博士学位论文

博士学位论文L’UNIVERSITECOMUEU NIVERSITEB RETAGNE L'Oire第601号博士学校数学与信息与通信科学与技术由古尔万·卡邦带注释语义的非局部分析认证论文于2018年12月14日在RENNES研究单位：Inria答辩前的报告员：Tamara Rezk，INRIA Sophia Antipolis-地中海Daniel Hirschkoff，LIP Lyon评审团组成：请注意，如果审查员：Sophie Pinchinat，INRIA雷恩Arthur CHARGUERAUD，Iniria ICUBE，斯特拉斯堡大学SylvainCONCHON，LRI巴黎南部Dir.论文作者：Alan Schmitt，INRIA雷恩3一个知识分子首先，我要感谢Daniel Hirschkoff和Tamara Rezk同意提交我的论文。我还要感谢Sophie Pinchinat、Arthur Charguéraud和Sylvain Conchon在我特别感谢他们五人对我的工作的兴趣和他们的相关反馈。如果没有我的论文导师艾伦·施密特，这项工作就不可能发生，他在我怀疑和恐慌的时候给了我自信的指导。他的帮助，这是科学的，我也要感谢凯尔特队的所有成员他们知道如何使我们共同的工作环境愉快我感谢其他博士生和博士后：马丁·博丹（Martin Bodin）、波琳·波利尼亚诺（Pauline Bolignano）、亚历山大·邓（Alexandre Dang）、斯特凡尼亚·邓布拉瓦（Stefania Dumbrava）、扬·费尔南德斯·德雷塔纳（Yon Fernándezde Retana）、蒂莫西·豪德堡（Timothée Haudebourg）、雷米·胡廷（RémiHutin）、文森特·拉波特（Vincent Laporte）、让-克里斯托夫·莱谢内（Jean-Christophe Léchenet）、朱利安·莱皮勒（Julien Lepiller）、谢尔盖·伦格莱（Sergei Lenglet）、托马斯·鲁比亚诺（Thomas Rubiano）、弗洛朗·索德尔（Florent Saudel）、阿利克斯·特里厄（Alix Trieu）、皮埃尔·威尔克（Pierre Wilke）和雅尼克·扎科夫斯基（Yannick Zakowski）特别感谢David Cachera，我和他一起迈出了我在教育界的我非常感谢我的父母也非常感谢Meven、Enora和Riwal，即使我是你们中最大的，你们也无法想象你们让我成长了如果没有许多朋友，我永远不会走到今天，首先，非常感谢Metig举办的所有这些4非常感谢你在一个系列节目前教我汉堡包如果没有洛伊扎的陪伴，如果没有我们的象棋比赛，如果没有我们的科学和哲学对话，如果没有她总是明智的建议，我就不会相信你的手臂!我还要感谢Maurine，我和她一起我永远也要感谢雨果，他总是在那里，一起学习，伸出援手，或者只是为了不用说，我感谢马尔福伊帮助我坚持下去，也感谢他我想从心底里感谢卡米尔，我每天都和他分享我的论文，特别是在这三年里，他作为一个室友成功地支持了我感谢埃莱娜一直在我身边，感谢她给我的支持除了小饼干，我知道你会记得，像我一样，我们分享的时刻最后，还要感谢Amelie Ga。Amelia Gu.，亚瑟，布鲁恩，伊芙，朱利安，梅文，摩根，劳伦特，托马斯，特里斯坦（以及其他许多人，我为没有提到他们而道歉），感谢他们各自的最后一次感谢和我在一起的毛茸茸的同伴。同居的机会感谢Belial和Maréchal Croquette（又名花栗鼠，又名冰箱，又名零食，又名软薯片，又名番茄酱蛋黄酱）为您的懒惰艺术。最后，我对蝙蝠侠有一个感人的想法，他的能量和不成比例的好奇心将留在我的5TABLE来自C组法文摘要导言111背景151.1不干扰151.1.1完成161.1.2不可决定性161.1.3流量模式171.1.4结论191.1.5相关工作201.2防鸡助手231.2.1一个证明助手231.2.2类型类251.2.3部分功能271.3漂亮的大步骤271.3.1什么是PBS？........................................................................281.3.2优势311.3.3PBS 35中的While语言2语义学的通用格式2.1动机412.2正式的漂亮大步骤412.2.1PBS摘要2.2.2WHILE语言的具体化2.3结论5263多语义学533.1第53章第一次见面3.2规范结构56内容表3.3属性603.4WHILE 61的多语义学3.5结论654注释694.1建筑694.2WHILE 75的注释多语义4.3捕获遮罩804.4限制835正确性855.1假设855.2正确性定理915.3测试分析仪93结论97参考书目99APBS规则的怀尔在公鸡1077R总结法语中从计算机和医疗设备到手表和汽车，几十年来，软件在我们生活的各个方面都变得越来越重要。他们可以帮助我们的日常生活（家用电器，汽车等），使我们能够通过互联工具（计算机、智能手机、手表等）与他人交流并通过游戏、电影和音乐来娱乐我们这些变化无疑在许多领域对我们的生活方式产生了有益的影响：卫生、运输、科学、农业等。但是，我们不应该忘记，由于所采用的机制的复杂性，软件可能不会这些所谓的漏洞可能会产生严重的后果：它们可能是事故的原因，如1996年阿丽亚娜5号发射失败[31]，也可能是恶意攻击的漏洞，如2012年出现并于2014年披露的心脏出血漏洞形式化方法为了克服bug，计算机科学家测试技术的优点是，当检测到错误时，通常可以跟踪执行跟踪并自动返回解决错误所然而，这也有一个缺点：在一个程序中找不到bug并不能保证它没有 bug，因为在一般情况下，可能的执行次数是无限的相反，形式化方法允许证明属性并确保程序不表现出8法文摘要与测试方法不同，它们确保在运行被分析的程序时不会出现与被证明的属性相关的形式化方法的另一个优点是虽然测试已经在行业中广泛使用了几十年，但形式化方法现在已经发展到足以与工业级项目的测试竞争：自2011年以来，亚马逊一直使用形式化规范和模型验证来解决现实世界隐私和数据由于软件无处不在，这意味着再加上这些工具通常能够将数据广播到通常有必要向软件提供一定量的数据以使其正常运行，但我们不希望这些数据被发送到例如，从浏览器登录其银行相反，一些软件的目的是接收数据，而不是 将 其 发 送 给 C’est le cas, par exemple, des bloqueurs de publicitésessayant de 这两个问题的共同点是管理软件中的数据流不干扰对数据流提供保证的一种方法是不干扰是一种安全属性，它保证回到在浏览器中输入密码的9法文摘要特定输出）不依赖于在银行网页的"密码"字段中输入的密码（特定输入）不干涉是一种超属性：[17]为了给属性一个反例，仅仅显示程序的特定执行（例如与非法内存访问相反）是不够的，而是通过比较至少两次执行的结果目标本论文的目的是提供一个框架来证明无干涉分析器。给定一种语言及其语义，我们的目标是建立一种替代语义，其中干扰可以通过单个派生来检测，从而允许对这样的派生进行简单的归纳考虑到原始语义的单次执行显然不足以确定程序是否是无干扰的令人惊讶的是，独立研究每个执行并收集依赖关系信息因此，我们提出了一种形式化的方法，它从尊重某种结构的任何语义中构造出一种多语义，允许在几个执行上同时进行推理我们证明了我们的方法是正确的，即这使我们能够确信正确的分析，而不依赖于不干涉属性，而是依赖于注释的多语义学为了说明我们的方法，我们提出了一个小型的While语言及其语义，我们构建了它的注释多语义，我们证明了这种语言的解析器计划手稿的其余部分是用英语写的，分为以下章节：第一章介绍了初步的概念：不干涉，第二章10法文摘要将Pretty-Big-Step形式化为Coq和WHILE语言的一个具体示例第3章描述了如何自动构建多语义。第4章注释了这种多语义，并解释了注释是如何工作的最后，第5章证明了注释的正确性，并展示了如何使用注释的多语义来证明解析器。11一、引言从电脑到医疗设备，再到手表和汽车，几十年来，软件在我们生活的各个方面都占据了越来越大的位置。它可以帮助我们的个人日常生活（如家用电器、汽车等），通过互联工具（如电脑、智能手机、手表）与他人交流，并通过游戏、电影和音乐娱乐我们。这些变化无疑在许多领域给我们的生活方式带来了好处：卫生、交通、科学、农业... 但不应忘记的是，由于所涉及的机制的复杂性，软件可能不具有我们所期望的确切行为。这些所谓的漏洞可能会产生严重的后果：它们可能是1996年阿丽亚娜5号发射失败的事故原因，也可能是恶意攻击的后门，如2012年引入并于2014年披露的心脏出血漏洞，该漏洞允许攻击者从加密通信中空投和窃取数据形式方法为了克服bug，计算机科学家开发了旨在发现错误行为的测试方法。测试技术的优点是，当发现错误时，通常可以追溯其来源，并自动返回修复错误所需的信息。然而，这也有一个缺点：不解决程序中的bug并不能保证程序总是正确地运行，因为在一般情况下，所有可能的执行都是有限的。相反，形式化方法允许证明属性并确保程序可能没有某些行为。与测试方法不同，它们保证在执行分析的程序期间不会出现与已证明属性相关的错误形式化方法的另一个优点是它们不需要运行程序，而是依赖于纯数学工具。12简介虽然几十年来测试在工业中被广泛使用，但正式的方法现在已经发展到足以在工业项目中竞争测试：自2011年以来，亚马逊一直使用正式的规格和模型测试来解决现实生活中的挑战。隐私和数据保护软件无处不在，这意味着它可以访问越来越多的数据。再加上这些工具通常能够将数据广播到其他设备（例如，通过互联网）这一事实，这就提出了一个重要的隐私问题。有很多数据我们必须交给软件，但同时我们也不希望软件发送到任何例如，从浏览器登录到他/她的银行帐户的人肯定不希望他/她的密码通过互联网发送。相反，有一些软件的目的是接收数据，但不向用户显示数据例如，广告拦截器试图阻止不显示敏感内容的广告和家长安全工具这两个问题的共同点是管理软件中的无干扰对数据流提供保证的一种方法是确保无干扰。非干扰是一种程序安全属性，它保证程序的规范fi输出独立于规范fi输入。回到在浏览器中输入密码的例子，我们希望确保发送到不是银行网站的每个网站的数据（规格文件输出）不依赖于在银行网页上的"密码"字段中输入的密码（规格文件输入不干扰是一种超属性：不能通过展示程序的一次特定执行（不像非法内存访问），而是通过比较至少两次执行的结果来给出属性目标本文的目的是提供一个框架来证明无干扰分析器当我们被赋予一种具有语义的语言时，我们就在构建一种语言。13简介另一种语义学，其中可以通过单个推导来检测干扰，从而通过在这样的推导上进行归纳来实现简单的证明。考虑原始语义的单次执行显然不足以确定程序是否是非干扰的。令人惊讶的是，独立地研究每个执行并收集依赖性信息也是不够的。因此，我们提出了一种形式化的方法，它从任何符合某种结构的语义中构建一种允许同时对多个执行进行推理的多语义。向这个多语义体添加注释可以让我们捕捉到program的输入和输出之间的依赖关系我们证明我们的方法是正确的，即注释正确捕获无干扰。这使我们能够证明声音分析，而不依赖于非干扰特性，而是依赖于注释的多语义。为了说明我们的方法，我们提出了一个小的While语言及其语义，我们建立了它的注释多语义，我们证明了一个分析器在这个语言。大纲第1章介绍了与不干涉特性、防公鸡助手和漂亮的大步相关的一般背景知识。第二章给出了漂亮的大步的公鸡形式化和用这种形式化编写的具体WHILE语言第3章描述了如何在一个相当大的步骤中自动构建多语义学第四章注释了多语义学，并解释了注释机制。最后，第5章证明了注释的正确性，并展示了如何在分析器证明中使用该框架源代码每一个定理，引理，假设或结论，出现在论文中，并已形式化的公鸡来与一个符号，指示链接到在线证明脚本。15C第 1章B地面这第一章的重点是给一些背景的三个主要的事情：不干扰属性，公鸡证明助手和漂亮的大步骤语义。在整个文档中，我们将遵循图1.1 在任何歧义的情况下直接来自我们工作的符号在相应的部分中结束。— 对于任何函数f：E→F，和元素x>E，v>F，如果x = y，则f[x → v]表示函数y →v。f（y）其他方面— 对于任何函数f：E→F，和子集HE，f（H）是H到f的像。— 对于任何偏函数f：E→F，Dom（f）E表示f在其上结束的域;—符号：：用于向列表中添加元素，符号@用于它用于列表连接。FIGURE 1.11.1无干扰非干涉的静态分析起源于1977年的E.科恩[18]和D. E. [21]第22话他们都提出了静态方法来跟踪程序中敏感数据的该物业于1982年由J.A. Goguen J.Meseguer [23]如下：如果第一组用户使用这些命令所做的操作对第二组用户所能看到的操作没有影响，则使用特定命令集的一组用户不干扰另一组用户。16第1章这种形式化超越了编程语言领域，可以应用于网络安全、社交交互等领域。1.1.1定义在我们的例子中，我们没有为编程语言指定非干扰规范假设我们有一种编程语言，其中变量可以是私有的，也可以是公共的。我们说一个程序是非干扰的，如果对于最初同意公共变量的任何一对执行，那么公共变量的值在执行后是相同的。换句话说，改变私有变量的范围并不影响最终的公共变量或者换句话说，公共变量不依赖于私有变量：没有私有信息的泄漏定义1（终端不敏感无干扰-TINI）。 如果对于以公共变量中的相同值开始的任何一对终止执行，执行以公共变量中的相同值结束，则程序是非干扰的。此终结仅考虑终结程序执行。我们通过四个日益复杂的例子来说明私人信息可能发生的泄露以及如何检测到它们。在所有这些变量中，public是公共变量，secret是私有变量。如果我们回顾一下Goguen Meseguer的整理，第是私有变量，第二组是公共变量，-commands是语言术语注意第二组可以看到的是执行开始和结束时公共变量中的值，这一点很重要;它不包括执行期间发生的情况。1.1.2不可判定性在试图捕捉无干扰之前，有必要了解它有多难，我们表明它是不可决定的。为了证明非干涉性质是不可判定的，我们简化了知道171.1. 无干扰一个程序是对终止不敏感的，它不干扰已知是不可判定的停止问题。我们假设我们有一个算法来确定一个程序是否是TINI，然后我们构建一个新的算法来解决停止问题。让我们考虑一个程序P和程序的输入I。我们还考虑了两个变量public和private，它们没有出现在P和I中，分别是public和private。我们用这些元素构建程序PJ结束为P（I）;公共：=私有我们声称P（I）在且仅在PJ不是TINI时停止。— 在单手操作中，如果P（I）停止，则考虑两次执行（一次在private变量中为true，另一次在public变量中为false）将在public变量中以不同的值结束。这一点得到了以下事实的支持：P（I）的计算不会改变私有财产的价值，因为它TINI的收尾工作— 在另一只手上，如果P（I）不停止，则P j的所有终止执行的集合为空所以PJ是蒂尼。通过这种方式，我们可以构建以下算法来解决停止问题：输入：P、I如果A（P（I）;public：=private）则返回false其他返回true结束所以，蒂尼是无法决定的。知道TINI是不可判定的，就不可能有完整和正确的分析。1.1.3流动模式泄漏信息和使程序干扰（或不干扰）有不同的方法。为了介绍最初的想法18第1章在多语义学中，我们给出了可能泄露信息的程序模式的非详尽列表作为第一个简单的例子，图1.2中的程序显然是相互关联的：改变s的值会改变public的值。如果我们坚持定义，我们可以说这个程序是干扰性的，因为有两个执行在{public：true;private：false}和{public：true;private：true}环境 中 开 始 （ 其 中 公 共 变 量 的 值 是 相 同 的 ） ， 并 分 别 在 {public ：false;private：false}和{public：true;private：true}环境中结束（其中公共变量的值是不同的）。public：=secretFIGURE 1.2这是一个直接的信息流，因为秘密的值是直接分配给酒吧。不幸的是，直接飞行并不是唯一的干扰源。它也可能来自执行特定指令的上下文。例如，图1.3中的程序显示了一个具有间接流的程序。秘密的价值并不直接存储在公共记录中，但如果声明中的条件保证在每种情况下，秘密都得到公共利益的价值。一个人可以检测到interferenceb，并考虑到分配发生的上下文。此程序的任何单次执行都将见证干扰。如果保密thenpublic：=truellsepublic：=falseFIGURE 1.3191.1. 无干扰屏蔽另一个干扰源是不执行代码的一部分可以提供信息的事实。这通常称为掩蔽。图1.4的流程图说明了这一现象。在secret为false的情况下，公共变量未被修改，因此此执行不会见证干扰，即使在考虑上下文时也不会。另一个秘密为真的执行见证了干扰。检测干扰的另一种方法是考虑程序的所有可能执行public：=falseif秘密thenpublic：=trueelse跳过FIGURE 1.4不幸的是，这又是不够的。在最后一个例子中，在图1.5中，我们可以看到不存在flow可能出错的单次执行。我们将把这个例子称为运行例子。在secret=true的情况下，public依赖于y，它没有被执行修改。在另一种情况下，secret=false，public仍然依赖于y，而y又间接依赖于x，而x没有被执行 修 改 。 亨 斯 在 这 两 种 情 况 下 似 乎 都 不 依 赖 于 R&T 。 Y 和 ，wehavepublic=secret在两次执行结束时，因此秘密被泄露。独立地查看每个执行是不够的。1.1.4结论为了将信息的干扰作为执行的一种属性来检索，我们提出了一种不同的语义，其中多个执行被视为锁定步骤，因此一个执行可以组合由多个执行收集的 信 息 。 在 最 后 一 个 例 子 的 情 况 下 ， 我 们 可 以 看 到 x de-pendonsecretinthefirstexexutionatthe end ofthefirstif. 在第二个ex执行中，xm也依赖于secret，因为它不修改x20第1章x：=truey：=trueif秘密thenx：=falseelse跳过如果xtheny：=falseelse跳过public：=yFIGURE 1.5关于S/R/T的F/R关系中的泄漏。我们可以很容易地模仿这取决于x在两个ex执行s，hencepublict rsiti vely取决于secret.我们建议将非干涉超属性转换为有限语义的属性。我们的方法提供了对有限语义学进行归纳推理的能力，并为分析的正确性提供了结构形式证明。秘密=真x：=truey：=trueif秘密thenx：=falseelse跳过如果xtheny：=falseelse跳过public：=y机密=假x：=truey：=trueif秘密thenx：=falseelse跳过如果xtheny：=falseelse跳过public：=y公共=真public=false（已执行代码、未执行代码）FIGURE1.61.1.5相关工作