CT-ISG: Collaborative Research: Non-bypassable Kernel Services for Execution Security

社会依赖于许多工程系统，这些系统日益增加的复杂性和相互关联性反过来又增加了它们对对抗性攻击的脆弱性。 在许多这样的系统中，保护其计算的执行与确保其数据的安全性一样重要。 本文研究了如何在入侵攻击中保持系统的可生存性，即如何通过系统中的特定资源来隔离计算之间的交互影响，包括：灵活地规范计算执行约束的强制执行;在一个单一的调度程序下显式控制所有操作系统内核组件;详细的在线监控计算及其支持操作系统内核组件;自动学习以发现以前未知的计算之间的交互;以及正式建模和验证计算，执行约束，系统组件和资源。该项目的预期好处包括：一种新的方法，从对抗性攻击的影响，其中隔离可以灵活地根据必须满足的特定于系统的执行约束来强制执行，一个高质量的内核级调度和监控服务的开源软件实现，提供和测量这种不可旁路的隔离;新的正式模型，分析和方法，用于这些服务的可验证的正确配置和管理;以及对服务在各种对抗性攻击下保护计算免受干扰的能力的实证研究。

Society is dependent on many engineered systems whose increasingcomplexity and inter-connectedness have, in turn, increased theirvulnerability to adversarial attacks. In many of these systems,protecting the execution of their computations is as crucial asensuring the security of their data. This research investigates howto maintain survivable operation of such systems, even in the face ofinvasive attacks where computations are intentionally subverted tointerfere with other computations' execution constraints.The goal of this research is to develop new techniques for isolatingthe effects of interactions among computations through specificresources in these systems, including: flexible specification andrigorous enforcement of computations' execution constraints; explicitcontrol of all OS kernel components under a single scheduler; detailedon-line monitoring of computations and their supporting OS kernelcomponents; automated learning to discover previously unknowninteractions among computations; and formal modeling and verificationof computations, execution constraints, and system components andresources.The expected benefits of this project include: a novel approach tonon-bypassable isolation of computations from the effects ofadversarial attack in which isolation can be enforced flexiblyaccording to the system-specific execution constraints that must besatisfied; a high quality open-source software implementation ofkernel-level scheduling and monitoring services that provide andmeasure such non-bypassable isolation; new formal models, analyses,and methodologies for verifiably correct configuration and managementof those services; and empirical studies of the services' ability toprotect computations from interference under a wide range ofadversarial attacks.