Litmus: Towards a Practical Database Management System with Verifiable ACID Properties and Transaction Correctness

Existing secure database management systems (DBMSs) focus on security and privacy of data but overlook semantic properties, such as the correctness and ACID properties of transactions. Enforcing these properties is crucial to the functionality of applications. If these guarantees do not hold, catastrophic losses could result. To address this issue, we present Litmus, a DBMS that can provide verifiable proofs of transaction correctness and semantic properties including atomicity and serializability. Litmus features a co-design of both the database and the cryptographic parts. We evaluate a proof-of-concept prototype of Litmus on the YCSB and TPC-C benchmarks and show that under reasonable cryptographic assumptions it can process more than 15,000 transactions per second (txn/s) verifiably. Our result shows a promising practical direction considering that PayPal runs on average 115 txn/s and VISA 2000-4000 txn/s. The proof is about 30kB per verification batch and verifies with a constant time of 300 seconds. Litmus can extend to verify consistency as well.