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

社会依赖于许多工程系统，这些系统日益增加的复杂性和互联性反过来又增加了它们面对对抗性攻击的脆弱性。在许多这样的系统中，保护其计算的执行与确保其数据的安全一样至关重要。本研究探讨了如何维持这样的系统的生存运行，即使面对有攻击性的攻击，其中计算被故意破坏，以干扰其他计算的执行约束。本研究的目标是开发新技术，通过这些系统中的特定资源来隔离计算之间相互作用的影响，包括：灵活的规范和严格的执行计算的执行约束；在单个调度器下显式控制所有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.