Selective High Assurance (SHA): Low-Cost Practical Verification of Security Modules for Cybersecure Software Platforms
Abstract
Abstract Recent large-scale surveys of enterprise cybersecurity identify several alarming trends, including high-value penetrationsof both commercial and government enterprises by state-sponsored adversaries originating from Russia, China, Iran, and North Korea.We argue that these trends will inevitably lead to the development of commodity software defenses based on selective high assurancefor software products (i.e., separation and formal verification of small security-sensitive software modules) that can withstand advanced persistent threats -- an initial step in cybersecurity transition from a presumed-breach-and-recovery mindset to a breach-prevention-first mindset.Currently a presumed-breach-and-recovery mindset is adopted because many enterprises have huge backlogs of unremedied known vulnerabilities; e.g., backlogs of over 100,000 unpatched vulnerabilities, of which they can only patch less than half. Recent research also shows that using mature zero-trust architectures for security-breach restriction to a small locale and AI/ML tools for early breach detection can never minimize an enterprises# recurrent breach-recovery costs. These approaches enable the persistence of known unpatched vulnerabilities, which prevent recovery-cost minimization by insurance coverage; i.e., no insurance company can provide coverage for security breaches caused by such vulnerabilities, particularly in state-sponsored attacks. A different approach to minimizing cybersecurity vulnerability and cost is thus necessary.Recent decreases in the cost of formal verification ofsecurity properties have reached the level where it becomes practical to prevent attacks by remote adversaries; e.g., these costs have decreased by nearly a factor of nine over the past decade. This means that tens of relatively small software modules (e.g., 75,000 source lines of code) of software services can be selected and formally verified to be penetration resistant against remote adversary attacks. Selective high assurance has two major additional cost advantages. First, its cost is incurred one time; i.e., it doesnot recur as in the case of breach recovery costs; and second it is more than dramatically amortized as it improves the security ofa large group of enterprises using the same software product. This project will illustrate the use of selective high assurance in practice. We will demonstrate how a formally verified, selected software platform can be protected from large, complex, and vulnerable commodity operating systems (OSes); e.g., Windows, Linux, or macOS, which are widely used by the US Navy. The project will demonstrate a low-cost formal verification of selected security modules running on commodity OSes that can withstand remote adversary attacks # even when these OSes are compromised by a remote adversary. To date, no low-cost formally verified security applications exist on insecure commodity OSes, which withstand remote state-sponsored attacks.Approved for Public Release
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Nov 08, 2024
- Source ID
- N000142412486
Entities
People
- Virgil Gligor
Organizations
- Carnegie Mellon University
- Office of Naval Research
- United States Navy