DivA: Automated Generation of Logical Code Diversity

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.