Beyond Algorithmic Proofs: Towards Implementation-Level Provable Security

TL;DR

This paper introduces Implementation-Level Provable Security, a framework for verifying security at the system implementation level, demonstrated through SEER, a ransomware-based file destruction system with practical security guarantees.

Contribution

It proposes a new paradigm for security verification at the implementation level and demonstrates it with SEER, integrating key erasure, entropy validation, and attack surface checks.

Findings

SEER achieves strong irrecoverability guarantees.

SEER maintains practical performance.

The framework shifts focus to verifiable implementation-layer security.

Abstract

While traditional cryptographic research focuses on algorithm-level provable security, many real-world attacks exploit weaknesses in system implementations, such as memory mismanagement, poor entropy sources, and insecure key lifecycles. Existing approaches address these risks in isolation but lack a unified, verifiable framework for modeling implementation-layer security. In this work, we propose Implementation-Level Provable Security, a new paradigm that defines security in terms of structurally verifiable resilience against real-world attack surfaces during deployment. To demonstrate its feasibility, we present SEER (Secure and Efficient Encryption-based Erasure via Ransomware), a file destruction system that repurposes and reinforces the encryption core of Babuk ransomware. SEER incorporates key erasure, entropy validation, and execution consistency checks to ensure a well-constrained, auditable attack surface. Our evaluation shows that SEER achieves strong irrecoverability guarantees while maintaining practical performance. This work demonstrates a shift from abstract theoretical models toward practically verifiable implementation-layer security.