Verifiable Software Diversity

Abstract

Software diversity promises fault tolerance by replacing dependence on single software paths with populations of alternatives that can be compared, switched, or voted upon. Realizing this promise requires more than nominal variety: the alternatives must satisfy a common behavioral contract and exhibit useful failure separation under relevant conditions. In distributed deployments, diversity may also exist only in name when participants cannot demonstrate that the claimed variants were actually built or executed. The first problem demands empirical validation; the second demands verifiable provenance.

This thesis proposes a framework for verifiable software diversity built around an evidence chain. The chain consists of four links: evidence that distinct variants exist for a given specification; evidence that they are substitutable for a defined purpose; measurements of their failure relationships under relevant conditions; and provenance checks connecting the claimed variants to the artifacts actually produced and deployed. Each link supports a distinct claim and cannot stand in for the others. In particular, provenance does not prove correctness or reliability, while source-code diversity does not prove behavioral equivalence or failure independence.

The five included works develop methods for gathering and validating evidence at each link. They study naturally occurring diversity among blockchain clients and diversity generated by large language models and coding agents. Compilation, testing, equivalence checking, and diversity measurement determine whether candidate versions are substitutable. Coincident failures, failure correlations, and majority-vote behavior characterize failure separation. Trusted execution and zero-knowledge proofs make claims about software use and compilation independently checkable. The studies also examine the operational costs, trust assumptions, and incentives that determine deployment feasibility.

The results show that verifiable software diversity is feasible and useful, but its benefits are not free. Independently developed and generated variants can provide meaningful diversity, redundant execution can improve availability or reduce observed failures, and verifiable provenance can make claims about diverse software use independently checkable. However, these gains require additional resources for redundant execution, effort to generate and validate variants, and computation to produce and verify provenance evidence. With these trade-offs made explicit, verifiable software diversity offers a practical path toward software systems that are both more reliable and more auditable.

Link to DiVA