Development Fund Proposal Submission - DamlSec
SubmittedPR- SIG
- needs-SIG
- Champion
- —
- Author org
- Dedaub Limited
- Ask
- 250,000
Abstract
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.
Milestones
| Title | Due date | Target | Amount (CC) |
|---|---|---|---|
| Core Symbolic Engine | — | — | 80,000 |
| Security Property Detectors and Counterexample Generation | — | — | 100,000 |
| CLI, Integration, Documentation, and Community Onboarding | — | — | 70,000 |
| Total | 250,000 | ||
Budget impact
- % of available
- 0.1%
- % if all RFV pass
- 0.1%
- Ask (CC)
- 250,000
Comments by org
No public reasons documented.
View discussion on GitHub