Development Fund Proposal Submission - DamlSec
RejectedPR- 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 approved-to-date
- 0.3%
- % if all RFV pass
- —
RFV scenario unavailable — using approved-to-date as denominator (degraded mode).
- Ask (CC)
- 250,000
Comments by org
2 comments · 2 orgs · last activity Oct 22, 2026
| Organisation | Comments |
|---|---|
| Dedaub | 1 |
| Canton Foundation | 1 |