Curry and TARTS with JP SMITH | CypherCon 1.0

### Overview In this talk presented at CypherCon 1.0, JP Smith discusses the fundamental challenge of reasoning about software behavior and guaranteeing correctness. While software behaves one way in a developer's mind or during testing, real-world execution on production hardware can behave very differently. Using side-channel timing attacks as a prime motivating example, Smith explores how conventional testing methodologies fall short and presents formal verification through dependently typed programming languages as an alternative method to mathematically prove code security properties.

### Key Topics - **The Problem of Program Reasoning**: Discrepancies between theoretical code design, developer intent, development environments, and actual production behavior. - **Side-Channel Timing Attacks**: How non-functional execution details (time, power, CPU operations) expose vulnerabilities in cryptosystems even when mathematical encryption cannot be directly reversed. - **Limitations of Traditional Assurance**: Why code review, unit testing, property-based testing, and fuzzing fail to guarantee security across all possible input domains. - **Type Systems as Logical Propositions**: The concept that types represent propositions and program terms represent proofs, which compilers verify. - **Dependent Types and Proof Assistants**: Applying languages like Idris, Agda, and Coq to encode and formally verify complex properties, including constant-time cryptographic operations.

### Technical Details Smith illustrates timing attacks using a naive byte equality function that loops bit by bit and stops early on the first mismatch. Comparing bytes that differ only at the end takes more loop iterations and time than comparing bytes that differ at the first bit. An attacker querying a password checker can evaluate response times to reveal each bit successively in O(n) time, effectively executing a binary search over secret data. Smith cites historical milestones where timing attacks broke production cryptosystems: - In 1999, Kocher broke RSA. - In 2003, Boneh and Brumley broke SSL. - In 2005, timing attacks broke AES.

Traditional testing covers only a subset of potential inputs and assumes malicious actors will not uncover degenerate paths. In contrast, formal verification leverages type systems where propositions correspond to types and functions serve as proofs. In dependently typed languages (such as Idris, Agda, and Coq), types can depend on values, allowing programmers to formulate arbitrary propositions—from the Pythagorean theorem to runtime guarantees.

Smith demonstrates modeling an equality function returning both a boolean bit and an operation counter (a natural number representing execution time). By formulating a dependent type stating that for any bytes `a, b, c, d`, the time to compare `(a, b)` equals the time to compare `(c, d)`, the compiler can verify that the comparison runs in constant time across all inputs, mathematically ruling out timing-based side channels.

### Takeaways - Standard testing only asserts that software works in tested scenarios, which provides insufficient protection against adversarial exploitation. - Dependently typed languages enable developers to turn code verification into proof checking, ensuring properties hold for all inputs rather than a sampled set. - While formal proof techniques provide absolute guarantees, Smith cautions that current tooling (Idris, Agda, Coq) primarily resides in academia and is not ready for mainstream production deployments. - Shifting security mindsets from "we tried hard to break it and failed" to "we proved it cannot break under any circumstances" offers a powerful theoretical direction for high-assurance software.