DivA: Automated Generation of Logical Code Diversity

Award Information
Agency:
Department of Defense
Branch
Navy
Amount:
$149,967.00
Award Year:
2011
Program:
STTR
Phase:
Phase I
Contract:
N00014-11-M-0280
Award Id:
n/a
Agency Tracking Number:
N11A-023-0140
Solicitation Year:
2011
Solicitation Topic Code:
N11A-T023
Solicitation Number:
2011.A
Small Business Information
33 Thornwood Drive, Suite 500, Ithaca, NY, -
Hubzone Owned:
N
Minority Owned:
N
Woman Owned:
N
Duns:
101321479
Principal Investigator:
DavidGuaspari
Senior Staff Scientist
(607) 257-1975
davidg@atc-nycorp.com
Business Contact:
RichardSmith
Controller
(607) 257-1975
rick@atc-nycorp.com
Research Institute:
Cornell University
Linda Brainard
Office of Sponsored Programs
373 Pine Tree Road
Ithaca, NY, 14853-
(607) 255-7123

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.

Agency Micro-sites


SBA logo

Department of Agriculture logo

Department of Commerce logo

Department of Defense logo

Department of Education logo

Department of Energy logo

Department of Health and Human Services logo

Department of Homeland Security logo

Department of Transportation logo

Enviromental Protection Agency logo

National Aeronautics and Space Administration logo

National Science Foundation logo
US Flag An Official Website of the United States Government