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

社会依赖于许多工程系统，这些系统日益复杂和相互关联，进而增加了它们对对手攻击的脆弱性。在许多这样的系统中，保护其计算的执行与确保其数据的安全同等重要。这项研究的目的是开发新的技术，以通过在这些系统中通过特定的资源来隔离计算之间的交互的影响，包括：计算执行约束的灵活规范和严格执行；在单个调度器下对所有OS内核组件的显式控制；详细的计算及其支持的OS内核组件的在线监控；自动学习以发现计算之间先前未知的交互；以及对计算、执行约束以及系统组件和资源的形式化建模和验证。该项目的预期好处包括：一种新的方法将计算与对抗性攻击的影响进行不可绕过的隔离，其中可以根据必须满足的系统特定的执行约束灵活地实施隔离；提供并测量这种不可绕过的隔离的内核级调度和监控服务的高质量开源软件实现；用于可验证地正确配置和管理这些服务的新的形式化模型、分析和方法；以及对服务在广泛的对抗性攻击下保护计算免受干扰的能力的实证研究。

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.