Audit
Audit Report
The PiggyBank program underwent security audit by Formal Land an auditing company that managed the formal verification of Tezos with Nomadic Labs.
The report is available here.
Audit Scope
The audit covered:
Program logic correctness
State transition safety
Access control mechanisms
Token handling security
Mathematical calculations
Edge case handling
Key Findings
Critical Issues
None identified.
High Severity
None identified.
Medium Severity
Integer Overflow Protection
Status: Resolved
Added checked math operations
Implemented overflow guards
Reentrancy Guards
Status: Resolved
Added state checks
Ordered operations correctly
Low Severity
Input Validation
Enhanced parameter checks
Added bounds validation
Improved error messages
PDA Derivation
Standardized seed usage
Consistent bump handling
Clear derivation patterns
Security Features
Access Control
Program implements strict access control:
Admin-only operations protected
User operations validated
PDA ownership verified
State Integrity
State transitions maintain invariants:
Balance consistency
Supply tracking
Redemption accounting
Token Safety
Token operations secured:
Authority validation
Amount verification
Decimal handling
Recommendations Implemented
Code Quality
Added comprehensive comments
Improved error handling
Enhanced logging
Testing
Expanded test coverage
Added fuzzing tests
Stress testing scenarios
Documentation
Clarified invariants
Documented assumptions
Added integration guides
Ongoing Security
Monitoring
Continuous security monitoring:
Transaction monitoring
Anomaly detection
Performance tracking
Updates
Security maintenance plan:
Regular dependency updates
Patch management
Vulnerability scanning
Future Audits
Planned security reviews:
Second audit scheduled
Continuous assessment
Community review program
Auditor Information
Auditor: Former Nomadic Labs engineer Background: Formal verification of Tezos Audit Date: October 2024 Methodology: Manual review + formal methods
Contact
For security concerns:
GitHub Issues (public)
Security email (private)
Bug bounty program (planned)
Last updated