用于保护操作系统安全属性的形式化方法

用于保护操作系统的安全属性的形式化奥尔良大学（University of Orleans）科学与技术博士实验室：LIFO论文提交人：乔纳森·鲁佐-科尔纳巴斯支持日期：2010年12月2日获得学位：奥尔良大学博士学位学科：计算机科学论文指导人：Christian TOINARD教授，LIFO（主任）Patrice CLEMENTELIFO高级讲师（共同负责人）报告员：Francine KRIEF教授，LABRIJean-Yves Marion教授，洛里亚陪审团：Mathieu BLANC博士，CEA-DAMPatrice CLEMENT教授，来自布尔日Francine KRIEF教授，ENSEIRBSébastien LIMET奥尔良大学教授Jean-Yves MARION南锡矿业学院教授Christian TOINARD教授，来自布尔日谢谢你我感谢弗朗辛·克里夫女士和感谢Jean-Yves Marion同意我想感谢我的博士论文评审团成员马修·布兰科先生劳伦特·克莱维耶先生塞巴斯蒂安·利梅特。我要感谢我的论文导师M.克里斯蒂安·托伊纳德和M. Patrice Clemente，我的共同负责人，感谢他们在我的研究期间的支持和帮助，感谢他们为我提供了完成这篇论文的机会，感谢中心地区和LIFO资助了这篇论文，从而使我能够进行这项研究。我也要感谢M.感谢Jeremy Briffaut在我整个论文过程中的帮助和支持。我要感谢安全和系统分发团队的所有成员帕斯卡尔·伯托姆M. 让-弗朗索瓦·拉朗德和M.Yacine Zemali和M.Martial Szpieg教授在我还要感谢我要感谢我的朋友和家人的鼓励和支持，最重要的是，我要感谢我的妻子斯蒂芬妮·奥利耶在我的论文中多次重读和支持4目录1引言152最先进2.1安全政策192.1.1安全政策202.1.2一般安全属性212.1.3衍生安全属性232.1.4讨论252.2保护模式252.2.1自由裁量访问控制2.2.2代理访问控制2.3以系统保护为导向的安全目标332.3.1自动机建模332.3.2完整性和保密性342.3.3信息流控制2.3.4滥用特权392.3.5特权的分离402.3.6竞争情况412.4结论423活动的形式化语言3.1操作系统实体3.1.1安全环境453.1.2基本操作463.1.3日期473.1.4事件和日期483.2基本行动493.2.1互动493.2.2交互标记503.2.3痕迹523.2.4直接信息流3.2.5直接信息流3.2.6多个直接信息流3.2.7一般直接信息流3.3间接信息流3.3.1因果依赖关系563.3.2定义573.4一般信息流3.5活动描述语言54安全属性的形式化4.1导言634.2通过过渡执行634.2.1间接执行634.2.2一般执行644.3完整性654.3.1对象的完整性654.3.2受试者的完整性674.3.3一般完整性684.3.4竞争形势704.3.5域的完整性704.3.6可执行文件734.4保密性764.4.1数据的保密性764.5多级安全（MLS）784.5.1Bell LaPadula限制型海滩784.5.2扩展794.6滥用特权814.6.1特权的分离814.6.2缺乏背景变化814.6.3遵守4.7动态属性844.7.1中国长城844.7.2动态数据遏制：一种新的动态保护模型..........................................................864.8结论935语言的实现5.1导言955.2交互图5.3信息流图5.3.1信息流图5.3.2增强的信息流图5.3.3不同图形的复杂性985.4100名操作员的实施5.4.1直接信息流5.4.2查找间接信息流5.4.3搜索所有间接信息流5.4.4一般流程1045.5编译语言1045.5.1编译我们的语言的通用方法1045.5.2安全属性示例1065.6结论1076实施和试验1096.1导言1096.2实施1096.2.1全球架构1096.2.2完整性110材料表76.2.3SELinux 1126.2.4PIGA-DYN-保护1126.2.5PIGA-DYN 1126.3实验1136.3.1蜜罐客户端1136.3.2蜜罐服务器1176.4结论1197结论1218附件1338.1 MLS 1338.1.1BIBA 1338.1.2带136级8.1.3贝尔·拉帕杜拉1388.1.4Bell LaPadula限制性1398材料表图表2.1表示系统状态的有限状态自动机示例........................................................................... 202.2表示系统安全状态的动态有限状态自动机示例2.3访问分离的表示302.4Apache 32的DEP配置3.1不同的基本操作集3.2系统调用的进入和退出事件的操作方案开放483.3交互表示..................................................................................................................3.4交互表示3.5T52轨迹的表示3.6信息流表示..............................................................................................................3.7标记的直接信息流表示阅读，2819，2973）543.8表示多个直接信息流阅读，2819，3254）553.9单信息流3.10 交互类型写然后读/间接信息流3.11 A和B之间的所有时间排序实例3.12 表示从csapache到csphp......................................................................................................................................60的4.1cs apache 64间接执行cs var _ www _ php的表示...........................................................................4.2具有直接和间接完整性中断的系统跟踪的表示664.3具有完整性中断的系统跟踪的表示4.4具有主体和客体完整性中断的系统跟踪的表示4.5具有并发情况的系统跟踪的表示4.6具有域中断的系统跟踪的表示4.7带TPE 75中断的系统轨迹表示4.8具有直接和间接保密性中断的系统跟踪的表示4.9BLPRP 79中断的系统跟踪表示.........................................................................................................4.10 具有特权分离中断的系统跟踪的表示4.11 具有上下文改变属性中断的系统跟踪的表示4.12 中国长城86无断裂系统轨迹的表示4.13 符合动态约束的系统跟踪的表示4.14 具有动态约束中断的系统跟踪的表示4.15 具有动态约束中断的系统跟踪的表示5.1交互图910图表5.2GFI列表5.1 975.3GFIA列表5.1 985.4在增强信息流图101中搜索5.5在增强信息流图104中搜索所有流6.1我们的保护系统的整体架构1106.2111呼叫转移系统的完成6.3PIGA-DYN-Protect 113内核模块的功能6.4GNU/Linux和Mo-下的高交互性HoneyPot客户端架构Mozilla Firefox 1158.1Biba 134断裂的系统迹线表示8.2不违反Biba 135第二规则的系统跟踪表示8.3不违反Biba 135第3条和第2条规则的系统跟踪表示8.4BLPR 141中断的系统跟踪表示..............................................................................................................8.5不违反BLPR 142第一条规则的系统跟踪表示8.6不违反BLPR 142的第一和第二规则的系统跟踪的表示算法列表1用于检测从CS1到CS2的间接信息流的算法在GFIA图中：searchUnFluxIndirectGraph（cs1，cs2，GFIA，direct）1022用于在标记为ite 1和GFIA图的交互中检测间接信息流fii 1的算法3用于搜索表示间接信息流的路径的算法在GFIA105图中从cs1到cs2的4CSS对象的一般完整性属性的实现算法反向cso：intObject（css，cso，ite1，GFIA）1065一种应用ac-无并发特性的优化算法通过mcs访问lcs：rapideNoConcurrenceAcces（lcs，mcs，ite1，GFIA）1071112算法列表图片列表4.1与图4.13相关的不同领域表 914.2与图4.14相关的不同领域表 924.3与图4.15相关的不同领域（和子领域）表935.1各种图形的复杂性995.2植入的功能及其检测到的内容6.1带有Mozilla Firefox 116的6.2SSH没有密码和登录117中的6.3phpBB和RoundCube与远程Shell执行缺陷1196.4Samba远程Shell执行1198.1完整性等级表8.2完整性等级范围表8.3敏感度/适应性等级表1401314表列表第一章简介每天的新闻都显示出信息系统的巨大脆弱性。我们可以在不同的使用环境中给出三个例子从互联网用户的工作站窃取信息的情况每天都在发生首先，在部署在客户端（公众、企业和政府）的大型信息窃取网络（僵尸网络）建立后，逮捕行动经常发生在实践中，通过社会工程，用户被引导执行恶意程序（恶意软件），然后检索个人或机密信息。第二个示例涉及通过客户端工作站访问公司Intranet的攻击场景。事实上，内联网的入口点正变得越来越强大。因此，客户端成为公司整体安全中最薄弱的环节。C’est ainsiquel’attaquenomméeOpérationAuroravisant Google(et d’autresgrandessociétésaméricaines)这两个示例说明了客户端安全问题的重要性。事实上，同一个工作站将用于各种用途。因此，有必要能够定义不同的域，例如用于Web浏览器，每个域都具有专用的安全目标此外，控制这些域之间的流量以确保与这些域相关联的安全目标也很重要。第三个示例说明了服务器的漏洞Web服务器攻击的案例每天都在发生这些服务器特别容易受到攻击，因为这些服务器上的风险更大，因为它们用于托管用途不兼容的各种应用程序因此，我们看到需要在信息系统的关键环节之一是操作系统。目前，操作系统是最薄弱的环节。事实上，它们目前无法为自己提供有效的保护，尤其是为它们所承载的应用程序提供有效的保护实际上，不可能为应用程序定义所需的安全目标，以便操作系统保证这些目标目前，主要的保护模式是自由裁量模式，其中最终用户定义对其资源的权限在这种模式下，不可能保证安全目标代理方法旨在允许定义安全目标，以便操作系统可以保证这些目标我们的最新技术水平将表明，所提出的方法非常部分地解决了1516第一章。引言适用于系统保护或者，他们计划对所有数据进行着色，以控制信息流或者，它们定义非常精细的保护策略，以处理进程对资源的权限。在这两种情况下，这都导致了显著的复杂性，并且不允许有效地处理传递信息流我们认为，基于病毒或行为分析的方法不适合系统保护。它们目前用于保护操作系统，这一领域的工作在极少数情况下，它们分析传递信息流然而，这项工作这些方法是对我们的方法的补充它们超出了本研究的范围，但我们将展示我们的结果在这些领域的应用前景目前，还没有足够开放和可扩展的解决方案来支持不同的域可以共享相同的基础架构，无论是客户端还是服务器，同时有效地控制域内部和域之间的信息流。C’est 本论文与2009年b]，安全挑战赛冠军她对这个项目做出了部分贡献它解决了在实际规模上实施深度保护系统的某些困难。事实上，安全挑战的一个教训是需要深度保护，即在操作系统的所有级别（内核、网络、用户界面、应用程序深入方法的困难在于能够将不同的保护策略与不同的使用领域相关联。因此，我们需要动态性在两个层面上运作。在最高级别，它是关于动态地定义不同域的安全目标。在较低级别，操作系统必须动态地确保这些安全目标。这两个层次是相互联系的。实际上，安全目标的动态保证允许本论文旨在促进安全目标的定义。为此，我们提出了一种语言，它允许我们形式化操作系统需要保证的安全属性正是这些安全属性将所需的目标形式化。该语言基于一组多亏了这种语言，我们可以很容易地将文献的所有经典保护属性形式化这种语言非常开放。它允许您定义新的安全属性。因此，我们提出了一种可扩展的方法来描述所需的安全目标。我们定义了一种编译该语言的方法，用于分析用户进程发出的系统调用编译方法基于信息流图的构造该图的复杂性随系统上实体类型的数量而多项式化。实际上，它的规模仍然很小。该编译提供了我们的运算符的实现，使用函数来分析我们的信息流图这些函数及其结果的处理的复杂性都是多项式的。在实践中，它们的复杂性仍然很低，这使得我们建议实现此语言以保护 在两种类型（客户端和服务器）的高交互蜜罐上进行了大规模的实验客户蜜罐允许17与Web浏览器相关联的一组广泛的安全属性为了然而，我们表明，用于分析的属性服务器蜜罐测试我们的保护方法在一组服务上的有效性它表明，没有此保护的计算机会受到影响，而受我们的代理方法保护的计算机不会受到影响。本文件的其余部分第2章介绍了它的结论是需要第3章提出了一个操作系统的抽象模型第4章使用此语言来形式化一组广泛的安全属性我们展示了它的表达能力第5章定义了我们动态编译安全属性的方法。它提出了一种基于信息流第6章介绍了基于我们的属性表达式语言的代理系统的实现他详细介绍了我们的蜂蜜罐的实验和结果。它不仅在性能方面，而且特别是在防止已知和未知攻击场景方面显示了有效性18第一章。引言第二章最新技术水平机密性和关于计算机系统安全评估标准[TCSEC，1985]（可信计算机系统评估标准-TSEC），美国国防部（DoD）出版了一本书（Orange Book），强调了安全政策的必要性这些政策必须能够 这些标准后来被一个欧洲国家委员会采纳为《信息技术安全评估标准》（ITSEC，1991）。本章介绍了与本论文目标相关的现有工作，即旨在使为此，必须能够容易地表达必要的安全属性。所使用的形式主义必须能够应用于经典的操作系统，如Unix。它应该能够正式化系统管理员和最终用户所期望的最广泛的属性。我们将把这种最先进的技术分为三个部分。首先，我们将重点讨论系统安全策略。第一部分将详细介绍系统可以保证的安全属性的主要类别。它将表明，这些类可以以不同的方式形式化，并且最后，它将以第二部分将介绍支持特定财产情况的经典保护模型。这一部分将表明，这一领域的工作既涉及财产的形式化，也涉及支持财产的手段。最后，它将表明，在第三部分中，我们将展示作者如何提出实现这些属性之一或这些模型之一。它将再次表明，所提出的解决办法不能轻易扩大，以实现我们的目标。在本章的最后，我们将解释在操作系统上形式化所需属性和保证这些属性时2.1安全策略安全策略的定义和这些目标可以以一组安全属性的形式来实现。每个属性都表示系统必须满足的一组条件，以保持在安全状态。不正确的定义或1920第二章最新技术水平图2.1不安全状态，允许信息或资源被盗、信息更改或系统在本节中，我们将首先解释什么是安全策略，然后定义我们在文献中遇到的不同类别的安全属性2.1.1安全策略安全策略指定了系统的"安全性它定义了对系统的期望的安全目标例如，它可以将来自特权域（例如：公司管理层）的所有信息不能被非特权域（例如：生产部门）读取作为隐私目标因此，这些目标对应于一组属性，这些属性可以以文学或正式的形式非正式地定义安全属性可分为三类[TCSEC，1985]：机密性、完整性和可用性。保密性是指对读取信息的访问控制完整性是关于写访问的至于可用性，它主要涉及服务的可属性可以指定允许或禁止的行为因此，可以还可以禁止非特权域访问此特权在大多数情况下，政策含蓄地认为，任何不允许的事情但是，在某些情况下，明确禁止的内容可能会有所帮助这种有利于授权的假设与一般规定禁令的立法方面相矛盾因此，检查或确保禁令和授权往往是必不可少的。在实践中，有必要能够保证禁令和授权。一般定义考虑一个信息系统在此表示中，我们可以通过以下方式定义安全策略：安全策略是将系统的状态划分为一组授权（或安全）状态和一组未授权（或不安全）状态的声明。因此，安全策略设置了可以将系统定义为"安全"的上下文定义2.1.2（安全系统）安全系统是指从安全状态开始，永远不会进入不安全状态的系统。