Skip to content

About

Binary-level assurance case study: byte-preserved OpenSSL caller proofs and review evidence; full replay distribution pending

Topics

Resources

Stars

0 stars

Watchers

0 watching

Forks

Repository files navigation

Binary Proofs: source and review edition

This repository contains selected, byte-preserved proof sources, caller sources, checking scripts, specifications, historical outcome records, and the C1/C2/C3 review packet. It is a source and review edition. Full replay assets are not published, and acquisition of the required replay assets is not presently complete. A clone of this repository cannot perform the sealed standalone replay described in the historical delivery documents.

Start with the human review packet, its literal contracts, and the case study draft. The authoritative release index identifies accepted packages, historical outcomes, and recorded later checking. Human review remains pending. This repository does not establish independent human or external organizational validation.

The bounded result is conditional composition through actual linkage for three experimental callers using unchanged production OpenSSL routines and supplier contracts, under pinned mathematical, fixed-image, and environment assumptions. Integration adaptation and caller-local proof work are disclosed. This does not establish arbitrary-caller integration, unrestricted processor or loader correspondence, a caller trace theorem, whole-library verification, comparative novelty, construction-cost savings, or amortization.

The original held-out C3 trial failed within its frozen construction limit; the original outcome record remains separate from the accepted C3 successor. The failed C1 predecessor and inspection-only C3 postmortem also retain their original identities. Later consumer receipts record checking-only acceptance for C1, C2, and the C3 successor; they do not revise the earlier failures or measure construction productivity.

Selected files retain their original repository-relative paths and exact bytes. Publishing this edition adds documentation and copies; it does not migrate or refactor original accepted proofs. Historical documents and seals keep their original versions, including references to assets omitted from this edition. The selection manifest records included hashes, source selections, explicit exclusions, and the identities of locally retained sealed assets.

Read publication scope and replay limitations before using checking instructions. Read the license and notice status before reuse. Original evidence contains local filesystem paths, hostnames, Docker identifiers, and socket paths; those historical bytes have been preserved. No additional license for the original project has been granted yet.

About

Binary-level assurance case study: byte-preserved OpenSSL caller proofs and review evidence; full replay distribution pending

Topics

Resources

Stars

0 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages