Development Fund Proposal Submission - DamlSec
Development Fund Proposal Submission
Proposal file:
/proposals/damlsec-dedaub.md
Summary
DamlSec is a symbolic execution engine for DAML-LF that automatically detects security vulnerabilities — authorization gaps, conservation violations, arithmetic faults, rounding errors, privacy leaks - by analyzing compiled .dar files across all feasible execution paths. It uses a two-tier SMT strategy with a pure-Scala inner prover for fast path pruning and CVC5 for heavyweight property verification and counterexample generation. No existing tool provides automated, path-sensitive security analysis that operates directly on compiled DAML artifacts.
Checklist
- Proposal file added under
/proposals/ - Milestones and funding amounts defined
- Acceptance criteria included
- Alignment with Canton priorities described
Notes for Reviewers
The tool reuses the Speedy Compiler pass and operates on compiled .dar artifacts, the same stable binary interface used by the rest of the Canton deployment pipeline.
- The inner theorem prover is pure Scala with zero native dependencies, making distribution as simple as any JVM artifact on the DAML toolchain.
- No existing tool fills this gap.
- Very limited execution risk.
- Dedaub has prior Canton/DAML audit experience and has built production-scale symbolic execution and static analysis tools for Ethereum used by over ten thousand registered users.