You are here

DivA: Automated Generation of Logical Code Diversity

Award Information
Agency: Department of Defense
Branch: Navy
Contract: N00014-11-M-0280
Agency Tracking Number: N11A-023-0140
Amount: $149,967.00
Phase: Phase I
Program: STTR
Solicitation Topic Code: N11A-T023
Solicitation Number: 2011.A
Timeline
Solicitation Year: 2011
Award Year: 2011
Award Start Date (Proposal Award Date): 2011-06-27
Award End Date (Contract End Date): N/A
Small Business Information
33 Thornwood Drive, Suite 500
Ithaca, NY -
United States
DUNS: 101321479
HUBZone Owned: No
Woman Owned: No
Socially and Economically Disadvantaged: No
Principal Investigator
 David Guaspari
 Senior Staff Scientist
 (607) 257-1975
 davidg@atc-nycorp.com
Business Contact
 Richard Smith
Title: Controller
Phone: (607) 257-1975
Email: rick@atc-nycorp.com
Research Institution
 Cornell University
 Linda Brainard
 
Office of Sponsored Programs 373 Pine Tree Road
Ithaca, NY 14853-
United States

 (607) 255-7123
 Nonprofit College or University
Abstract

Computing systems built on identical foundations (hardware, operating systems, etc.) will be vulnerable to the same attacks. To avoid widespread failures, techniques have been sought for introducing"synthetic diversity"into systems. The best studied are low level randomization techniquesfor example, pseudorandom run-time decisions that make it impossible for an attacker to predict how a program will be laid out in memory. ATC-NY and Cornell University will develop the DivA system to provide a fundamentally different, and complementary, logical diversityto generate modules that provide the same service by different computations. DivA exploits the constructive logic principle of"proofs as programs."To generate variant versions of a module, a developer creates an initial seed, implementing it as the program corresponding to a constructive proof; DivA uses heuristic methods to find alternative proofs of the same proposition, and therefore alternative implementations of the module. The NuPrl logical programming environment provides powerful support for creating the seed. By choosing from many versions of many modules, a system integrator or automated recovery mechanism can create a vast number of logically distinct versions of the same system. Testing them all is infeasible, but DivA justifies these combinations by providing strong guarantees of functional correctness.

* Information listed above is at the time of submission. *

US Flag An Official Website of the United States Government