SBIR Phase I: Secure Computing using Pluggable Trust Technology

这个小企业创新研究（SBIR）第一阶段项目的更广泛的影响/商业潜力是恢复对计算系统的信任。 成功的网络攻击，包括大规模隐私泄露和设备后门的发现，动摇了人们对计算的信任，使用户处于危险之中，损害了经济，甚至威胁到我们的国家安全。 通常的一套临时的、不完整的和昂贵的方法根本没有解决这个问题。 这项研究工作将推进一个可行的、实用的和整体的解决方案，为用户提供更强的安全保障，同时降低保持系统安全的成本。这个小企业创新研究（SBIR）第一阶段项目将开发TigerGuard，一个计算机系统安全架构，包含网络攻击对现有计算机基础设施的影响。 TrustGuard基于一个单独制造且易于验证的小型硬件元件，称为Sentry，它作为信任的根。 Sentry是一个通用的硬件信任组件，当与特定于应用程序的动态规范检查（DSC）软件组件结合时，它提供了灵活的包容能力。 尽管操作系统、固件、硬件和软件（包括应用软件本身）存在设计和制造缺陷（已知和未知，恶意和无意），TigerGuard的遏制保证仍然有效。Sentry和DSC的正式验证，考虑到它们的总大小只有几千行代码，在安全保证方面等同于证明数亿行现有代码的正确性（包括处理器设计，内存实现，硬盘驱动器固件，操作系统，共享库和应用程序代码）。

The broader impact/commercial potential of this Small Business Innovation Research (SBIR) Phase I project is the restoration of trust in computing systems. Successful cyberattacks, including mass privacy breaches and the discovery of device backdoors, have shaken trust in computing, put users at risk, hurt the economy, and even threatened our national security. The usual set of ad-hoc, incomplete, and costly approaches simply have not addressed the problem. This research effort will advance a viable, practical, and holistic solution that gives users much stronger guarantees of security while lowering the costs of keeping systems secure.This Small Business Innovation Research (SBIR) Phase I project will develop TigerGuard, a computer system security architecture that contains the effects of cyberattacks on existing computer infrastructure. TrustGuard is based on a small, separately manufactured, and easy-to-verify hardware element, called the Sentry, that serves as the root of trust. The Sentry is a general-purpose hardware trust component that, when combined with an application-specific Dynamic Specification Check (DSC) software component, provides flexible containment capabilities. The containment guarantees of TigerGuard hold despite design and manufacturing flaws (known and not-yet-known, malicious and unintentional) in the operating system, firmware, hardware, and software, including those in the application software itself. Formal verification of both the Sentry and DSC, a practical effort given their total size of only a few thousand lines of code, becomes equivalent in security guarantees to proving hundreds of millions of existing lines of code correct (including the processor design, memory implementation, hard drive firmware, the operating system, shared libraries, and the application code).