Finding Cross-rule Optimization Bugs in Datalog Engines

on YouTube ↗17m

" summary

Automated blackbox testing uses Incremental Rule Evaluation (IRE) to build Datalog programs rule by rule, evaluate each new rule in isolation as a reference, then compare to the engine’s optimized run to flag discrepancies. Implemented as Deopt, it runs against Soufflé, CozoDB, μZ, and DDlog and finds 30 bugs including 13 logic bugs, catches all queryFuzz bugs and five others queryFuzz misses, and produces 1.17×–31.02× more nonempty 60‑rule tests than naive random generation.

AI-written summary · about

" chapters (9)

1. 0:00Cross-rule optimization bugs
2. 3:15Logic bugs in Datalog engines
3. 5:00Incremental rule evaluation
4. 6:44Generating test cases
5. 9:59Rule dependencies and stratification
6. 12:33Evaluation results and bugs
7. 14:46Incremental vs random testing
8. 15:51Conclusion and future work
9. 16:14Q&A

" related talks

• 14mDetecting Logic Bugs in Database Engines via Equivalent Expression TransformationZhendong Su, Zu-Ming Jiang · 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24)
• 42mSurprise yourself with Property Based TestingMartin Hellspong · Øredev 2023
• 55mMuch ado about testingNicolas Rinaudo · ScalaIO 2019
• 15mFinding Bugs in Database Systems via Query PartitioningManuel Rigger, Zhendong Su · OOPSLA 2020
• 18mPreview: Verification (Correctness & Debugging)Chengcheng Wan, Lefan Zhang · OSDI '21 / USENIX ATC '21
• 36mSQLancer: Automatically Finding Bugs in Database Management SystemsManuel Rigger · SPLASH 2020 REBASE
• 19mPinolo: Detecting Logical Bugs in Database Management Systems with Approximate...Charles Zhang, Chengpeng Wang, Rongxin Wu, Zongyin Hao, Quanfeng Huang, Jianfeng Wang, Yushan Zhang · USENIX ATC '23
• 11mEncarsia: Evaluating CPU Fuzzers via Automatic Bug InjectionKaveh Razavi, Matej Bölcskei, Flavien Solt, Katharina Ceesay-Seitz · USENIX Security '25