Polysys: an Algebraic Leakage Attack Engine

Consider a scenario in which a hospital wishes to store their highly sensitive data on a third-party database server (such as AWS). Because they are afraid of scenarios such as data breaches or regulatory audits, the hospital will often store the data encrypted using a primitive…

Verified CNF Encodings

Boolean satisfiability, or SAT, is a classic computational problem: given a Boolean formula, determine whether there exists an assignment to the variables that satisfies the formula. SAT is NP-complete, meaning all problems in the complexity class NP can be (efficiently) translat…

Correctness of Compilation

Compilation is the process of converting a human-comprehensible, mathematically rich programming language into a machine-readable, operationally explicit target language, often involving multiple sequential phases. Compilation correctness ensures that the original program supplie…