问责制的正式模式瓦利德·本加布里特引用此版本：瓦利德·本加布里特问责制的正式模式计算与语言[CS.CL]。国立高等矿业电信学院，2017年。英语NNT：2017IMTA0043。电话：01692550HAL Id：tel-01692550https://theses.hal.science/tel-016925502018年1月25日提交HAL是一个多学科的开放获取档案馆，用于存放和传播科学研究文件，无论它们是否已这些文件可能来自法国或国外的教学和研究机构，或来自公共或私人研究中心。L’archive ouverte pluridisciplinaire博士论文瓦利德·本哈布里特Mémoire presenté en vue deBretagne-Pays de la Loire - IMT国立高等矿业-电信学院博士学位布列塔尼卢瓦尔大学校园École doctorale：Mathématiques et STIC（MathSTIC）学科：信息学，CNU27Spécialité：Sécurité et sancerreté de l'informationUnité de recherche：Le Atuatoire des Sciences du Numérique de Nantes（LS2N）发布时间：27/10/2017Thèse N°：2017IMTA0043联合国负责模式«问责制的正式模型»陪审团报告员：Ana Rosa CAVALLI女士，南巴黎M. Yves ROUDIER，尼斯大学教授，Sophia Antipolis审查员：M. Daniel LE METAYER，Directeur de Recherche，InriaNora CUPPENS女士，研究部，IMT ATLANTIQUEM. Anderson SANTANA DE OLIVEIRA，Chercheur Sénior，SAP实验室Director deThèse：M. Jean-Claude ROYER，IMT ATLANTIQUE矿业公司，Thèse公司共同负责人：M. Hervé GRALL，会议室主任，IMT ATLANTIQUEA FO R M A L M O D E L FO R A C C O U N TA B I L I T Y瓦利德本加布里特-Computer Science计算机ASCOLA研究小组主管：Jean-Claude Royer教授共同主管：A/Prof. Hervé Grall– OCT 2017Walid Benghabrit：问责制的正式模式，©“By the time I realized my parents were right, I had kids that didn’tbelieve-侯赛因·尼莎献给我的父母。A B标准如今，我们正在见证云服务的民主化因此，越来越多的最终用户（个人和企业）在日常生活中使用这些服务在这种情况下，个人数据通常在几个实体之间流动最终用户需要了解个人数据的管理、处理、存储和保留，并拥有必要的手段，使服务提供商对使用其数据负责在这篇论文中，我们提出了一个问责制框架，称为问责制实验室（AccLab），允许考虑问责制从设计时间到实施时间的系统。为了协调法律世界和计算机科学世界，我们开发了一种名为抽象责任语言（AAL）的语言，允许编写义务和责任政策。该语言基于一种称为一阶线性时态逻辑（FOTL）的形式逻辑，该逻辑允许检查问责制政策的一致性这些政策被翻译成一个时间逻辑称为FO-DTL3，这是与基于公式 重 写 的 监 控 技 术 。 最 后 ， 我 们 开 发 了 一 个 名 为 问 责 制 监 控（AccMon）的监控工具，它提供了在真实系统中监控问责制政策的方法这些策略基于FO-DTL3逻辑，框架可以在集中或分布式模式下工作，可以在在线和离线模式下运行。VIIR S U MNous assistons à la democratisation des services du cloud et deplus en plus在这些场景中，这些人在不同的人之间有着短暂的普遍关系。La responsabilisation（ou accountability）designe le fait qu在这方面，我们提出了一个AccLab责任化框架，该框架允许考虑到一个系统的概念阶段的责任化在与司法世界和信息世界进行协调后，我们提出了一种AAL语言，它渗透了责任义务和这种语言是以FOTL形式的一种逻辑为基础的，它允许验证负责制政治的一致性，即两种政治之间的兼容性。这些政策是在我们命名为FO-DTL3的一个逻辑上进行的，这一点与一种基于森林记录的监测技术有关。我们应加强对AccMon的监测，AccMon是一种在有关制度的背景下监测政治责任的手段政策的基础是FO-DTL3的逻辑，框架可以集中或分配方式，并在线上和线外发挥作用。VIIIP U B L I C AT I O N S这可能会对博士论文派上用场：一些想法和数字以前曾出现在以下出版物中：[BEN 15] Walid Benghabrit.« Framework pour la responsabilisa-tion.» In：Conférence en Ingénierie du Logiciel，CIEL 2015.法国波尔多，2015年6月。[BGR 16] Walid Benghabrit，Hervé Grall和Jean-Claude Royer。利用AccMon框架监测问责政策。GDR-GPL。海报2016年6[Ben+14a] Walid Benghabrit，Hervé Grall，Jean-Claude Royer，Mo-hamed Sellami，Monir Azraoui，Kaoutar Elkhiyaoui，Melek Önen ， Anderson Santana De Oliveira ， andKarin Bernsmed.云问责政策表示框架。»在：CLOSER -第四届云计算和服务科学国际会议。2014年4月，西班牙科隆。网址：https://hal.inria.fr/hal-00941872。[Ben+14b] Walid Benghabrit ， Hervé Grall ， Jean-Claude Royer ，Mo- hamed Sellami，Karin Bernsmed，and AndersonSantana De Oliveira.抽象的责任语言。»在：IFIPTM -第8IFIP WG 11.11信托管理国际会议.新加坡，新加坡，2014年7月。[Ben+14c] Walid Benghabrit，Hervé Grall，Jean-Claude Royer，andMohamed Sellami.«抽象组件设计的责任。»在：EUROMICRO DSD/SEAA 2014. 维罗纳，意大利，Aug.2014年，第页213-220 DO I：10. 110 9/SEA A. 2014年。68岁。网址：https://hal.inria.fr/hal-00987165。[Ben+15a] Walid Benghabrit，Hervé Grall，Jean-Claude Royer，andMohamed SELLAMI.摘要问责制语言：翻译，合规性和应用。»在：亚太软件工程会议.新德里，印度，2015年12月。网址：https://hal.archives-ouvertes。fr/hal-01214365。[Ben+15b] Walid Benghabrit，Hervé Grall，Jean-Claude Royer，andMohamed Sellami.“用一个证明者来检查责任»在：第39届IEEE COMPSAC. 2015年，第页83-88. DOI：10.1109/康普萨角2015年8 .第八条。 URL：http：//dx. 是的。或g/10。1109/COMPSAC.2015.8。IX[Ben+15 c] Walid Benghabrit， Hervé Grall ， Jean-Claude Royer，Mo- hamed SELLAMI ， Monir Azraoui ， KaoutarElkhiyaoui ， MelekOnen ， SantanaOliveiraDeAnderson，and Karin Bernsmed. 从监管义务到云中可执行的问 责政策。»在： 云计算 和服务科学。CLOSER2014，西班牙巴塞罗那，2014年4月3日至5日，修订论文集。瑞士施普林格国际出版社，2015年。网址：https：//hal.archives-ouvertes.fr/hal-01214387上下载。[SRB 14]Mohamed SELLAMI，Jean-Claude Royer和Walid Beng-habrit。“数据保护的责任。» In：国际多媒体理解. 11月15日，法国巴黎2014年。网址：https：//hal.archives-ouvertes.fr/hal-01084890上下载。XQ（λ x. x ∈ thanksList thanks（x））R E M E RC I E M E N T S“Nous sous-estimons trop souvent le pouvoir d’un contact, d’unsourire, d’un mot gentil, d’une oreille attentive, d’un complimentsincère,-利奥·布斯卡利亚C’est阿尔伯特·爱因斯坦曾经说过，一个人的价值在于他的能力，而不是他的能力杜兰特今年很荣幸地与我的导师让-克洛德·罗耶的一位有价值的人一起工作一个人的典范，一个追求职业的人。谢谢让-克劳德让我能在这几年里一直关注你我一直在安慰我的同伴埃尔韦·格拉尔等他离开我的时候。感谢埃尔韦让我继续关注，非常感谢Mario Südholt让我在Je remercie les membres de 特 别 是 Mohamed Sellami 、 MehdiHaddad、Rémi Douence、Jaques Noyé、Adrien Lebre、AlexandreGarnier 、 Rémy Potier 、 Simon Dupont 、 Kevin Quirin 、 SimonBoulier和Hugo Brunelière。感谢菲利普·大卫允许我担任教育工作，并提出关于学生中间方案的建议。感谢佛罗伦萨·罗格，凯瑟琳·富尔尼，索琳·普恩特·罗德里格斯和戴尔芬·图里尔，为您提供支持。非常感谢B231联合办公室的同事们，我是弗洛朗、罗南和约翰纳坦的朋友，这份工作非常丰富，非常感谢你们。感谢弗洛伦特、罗南和乔纳森的支持，感谢阿明、亚历山大、古斯塔沃、萨卡西奥、齐亚德和布里斯的参与。 里恩德Xi↓→↓→ ↓→↓→mieux pour décompresser que des ultraen“PP. . . P“还有肖柳在外面，如果肯和拉希德还不满足我感谢机器人俱乐部，扬，本尼迪克特，托马斯和安奇让我们一起走感谢杨先生对我们的讨论技巧和哲学，因为我们没有时间我感谢罗兰·杜库尔诺让我能继续研究，克莱门汀·内比和皮埃尔·蓬皮多尔让我能在鹰号上找到我感谢维克多·高格勒和丽塔·巴杜拉为我提供了良好的教育经验感谢安娜·罗莎·卡瓦利、伊夫·鲁迪埃、丹尼尔·勒·梅塔耶、诺拉·库彭斯、安德森·桑塔纳·德·奥利维拉，让我有幸成为这一案件的陪审团成员我很感谢我的家人，特别是我的祖母阿兹莎，我的叔叔查基布，还有我的朋友，特别是奥妮，埃迪和西尔维，为了我的安全谢谢阿德尔和我的长期朋友约会。谢谢雷米，维罗尼克，科拉莉，亚瑟和哈罗德给你们的支持也谢谢阿黛拉德给我的支持我会向我的母亲父亲和我的姐姐伊斯玛哈恩表示哀悼我会好好照顾你们的。XII公司简介我 责任： 超出 安全 和 隐私11介绍31.1动机. . . . . . . . . . . . . . . . . . . . . . . .31.2背景和问题。. . . . . . . . . . . . . . . . .41.3纲要. . . . . . . . . . . . . . . . . . . . . . . . . .52现有技术72.1导论.. . . . . . . . . . . . . . . . . . . . . . . .72.2计算机安全的神话. . . . . . . . . . . . .82.2.1 云，通过互联网和网络。. . .82.2.2网络攻击与网络防御 . . . . . . . .102.3隐私，数字世界中的幻觉。. . . . . . . . . .122.3.1什么是隐私？. . . . . . . . . . . .122.3.2 现实世界中的隐私：法律和法规。142.3.3实现隐私权的正式化。. . . . . . .152.4 责任：超越安全保护隐私。 . .162.4.1政策语言：建立世界之间的联系172.4.2 时间逻辑：物理世界的形式化。 . .18II问责：从规范到实施213一个摘要问责 语言233.1导论.. . . . . . . . . . . . . . . . . . . . . . . .233.2抽象责任语言（Abstract Accountability Language，AAL）. . . . . . .243.2.1 AAL语言语法。. . . . . . . . . . . . . .243.2.2时态逻辑：AAL语言的语义。.273.2.3 在AAL中表达安全和隐私。. . . .313.3在设计时处理责任。. . . . . . . . .323.3.1设计责任。. . . . . . . . . . . . . . . .323.4检查和证明责任。. . . . . . . . . .333.4.1模型检查与证明。. . . . . . . . . .333.4.2条款的一致性和合规性。 . . . . . .343.4.3冲突检测和定位。. . . . . . .353.5 AAL的高级用法。 . . . . . . . . . . . . . . . . . .363.5.1 可用性和开发扩展。. . . . .383.5.2扩大授权。. . . . . . . . . . . .403.5.3 AAL型系统。. . . . . . . . . . . . . . . . .423.6结论和讨论。. . . . . . . . . . . . . . . .444问责执法474.1导论.. . . . . . . . . . . . . . . . . . . . . . . .47XIIIxiv目录4.2从全球规格到地方规格484.3在运行时验证时态逻辑4.3.1监测一级病例504.3.2有限迹解释与三值逻辑504.3.3处理分配问题4.4FO-DTL3：一阶时间分布式逻辑514.4.1FO-DTL351的语法4.4.2FO-DTL352的语义4.5FO-DTL3监测4.5.1建筑工程544.5.2第一批订单和分销扩展574.5.3监控优化604.5.4监测的完整性和可靠性614.6使用FO-DTL.......................................................................................... 监控AAL策略4.7结论625问责工具5.1一、导言. 655.2AccLab：问责制实验室665.2.1框架介绍.665.2.2AccLabIDE675.2.3模拟和监测5.2.4用例725.3Fodtlmon：FO-DTL 3的监测框架755.4使用AccMon77监测问责制5.5PyMon：一个Python监控框架815.6结论83iii问责制：超越问责制856结论和今后的工作. 87iv附录93a开始使用ACCLAB95a.1安装AccLab95a.1.1使用AAL编译器“aalc”95a.1.2编写您的第一个AAL程序96a.1.3在命令行98a.1.4高级支票100a.1.5使用shell101BIBLIOGRAPHY书目105L I S T O F I G U R E S图1全球网络架构。. . . . . . . . . . . .11图2隐私意见-XKCD。 . . . . . . . . . . .13图3DTL监控示例。. . . . . . . . . . . .60图4AccLab工作流程。. . . . . . . . . . . . . . . .66图5AccLab架构。. . . . . . . . . . . . . . .67图6AccLab UI（组件图视图）。. . . .68图7AccLabUI概述。. . . . . . . . . . . . . .68图8AccLab仿真模型。. . . . . . . . . . . .69图9AccLab组件图编辑器。.72图10AccLab一致性检测。. . . . . . . . .74图11AccLab合规性检测。 . . . . . . . . .74图12AccLab模拟。. . . . . . . . . . . . . . .75图13Fodtlmon建筑。. . . . . . . . . . . . .75图14AccMon全球架构。 . . . . . . . . . .78图15AccMon架构。. . . . . . . . . . . . . .79图16AccMon监视器概述。. . . . . . . . . . .81图17AccMon跟踪。. . . . . . . . . . . . . . . . . .81图18论文推理流程。 . . . . . . . . . . . .88图19警察的警察。 . . . . . . . . . . . . . . . . .89L I S T O F TA B L E S表1命题逻辑语法。. . . . . . . . . . .18表2命题逻辑语义学. . . . . . . . . .18表3时态逻辑语法。. . . . . . . . . . . . .19表4一阶线性时态逻辑语法 . . .28表5FOTL上的AAL语义。. . . . . . . . . . .29表6 FOTL41上的AAL扩展授权语义FOTL42表8 AAL型系统43表9一阶分布式线性时序逻辑表10FO-DTL3的语义表11 LTL运算符的级数语义表12LTL_3的进展算法表13 Fodtlmon语法76XVL I S T I N GS清单1AAL核心语法。. . . . . . . . . . . . . . .27清单2数据保留示例。. . . . . . . . . . . . .31清单3数据传输示例。. . . . . . . . . . . . .31清单4数据主体明确同意示例。 . . . .31清单5违规通知示例。. . . . . . . . .31清单6AAL语法。. . . . . . . . . . . . . . . . .36清单7aalc期权. . . . . . . . . . . . . . . . . . .95A C RO N Y M S抽象责任语言WEB万维网HTML超文本标记语言HTTP 超文本传输协议SaaS软件即服务PaaS平台即服务IaaS基础设施即服务一阶线性时序逻辑AccMon 问责制监测AccLab清点实验室可扩展访问控制标记语言PII个人身份信息CSP云服务提供商GDPR一般数据保护条例GLBAGramm-Leach-Bliley法案受PHI保护的健康信息PDRM个人数字版权管理CNP着色Petri网后验线性时态逻辑SIMPLSIMple保密语言OSL义务说明语言IOT物联网sloc源代码行XVI第一A C C O U TA B I L I T Y：B E Y O N D S E C U R I T Y AD P R I VA C Y我们生活在一个机器在我们日常生活中无处不在的世界里，公鸡被闹钟和智能手机所取代，信件被电子邮件所取代，马被拥有复杂电子产品的汽车所取代计算机无处不在，21世纪的人类用它们来休闲、工作、交流甚至控制航天器。在这个数字信息无处不在的世界里，我们的个人数据不断暴露，那么我们的隐私呢我们的数据托管在计算机中并通过网络传输人类在计算机安全和隐私保护中的作用是什么？完美的安全性能保证我们的隐私吗？“Perfect系统”。- William D. 年轻I N T RO D U C T I ON1内容1.1动机. . . . . . . . . . . . . . . . . . . . .31.2背景和问题。. . . . . . . . . . . . .41.3概述。. . . . . . . . . . . . . . . . . . . . . . .5“Everybody with a computer should worry a little about- 约翰·维耶加1.1动机当我十四岁的时候，我通过黑客技术发现了计算机科学，我很惊讶我们可以通过使用黑客软件和脚本轻松进入计算机，而不需要很多知识在该领域 想想一个恶意的脚本孩子可以做什么在黑客文化中，这些工具很吓人我相信，一个密集的控制和强大的保护是所有这些安全问题的答案，但同时我知道，每次安全专家开发一个新的保护机制，黑客找到新的方法来绕过它。这我的导师告诉我，我们将致力于计算机安全和数据隐私，我对自己说：我们将找到最终的保护！通过报名参加这篇论文，我希望从事低级别的安全工作，开发新的保护机制和软件，但事实并非如此，至少在我的论文开始时。 在我第三年的中期，我们开始研究低级别的安全工具，那时我明白，如果我直接开始研究低级别的安全工具，就会缺少一些东西。事实上，当一个人或一家公司侵犯了我们的隐私，不尊重他们的隐私政策时，我们通常因此，隐私权侵犯问题不仅仅是一个低层次的安全问题，它还涉及到法律、经济和社会等多个方面。但是，在数字世界中保护我们的隐私真的那么重要吗？毕竟，谁在乎呢？3脚本小子是指使用其他黑客开发的脚本或程序来攻击计算机系统和网络的非熟练人员。
我的内容管理
展开
