Please report security vulnerabilities by opening a private GitHub Security Advisory at:
https://github.com/Utility-Drip/Utility-Drip-Contracts/security/advisories/new
Do not open a public issue for security-sensitive findings.
For every active stream:
current_time ≤ start_time + ⌊initial_balance / flow_rate⌋Equivalently,
calculate_remaining_balance(balance, rate, elapsed)never returns a negative value.
This invariant guarantees that the contract is insolvent-proof with respect to individual device streams: a stream can never pay for more seconds than its deposited balance allows.
Let:
B= initial balance (integer, stroops or token units)R= flow rate (integer, units per second,R > 0)T_max=⌊B / R⌋(maximum seconds the stream can run)C(t)= consumed at timet=R × t(integer multiplication)
Claim: B - C(T_max) ≥ 0
Proof:
T_max = ⌊B / R⌋
⟹ T_max ≤ B / R
⟹ R × T_max ≤ B (multiply both sides by R > 0)
⟹ B - R × T_max ≥ 0 (rearrange)
⟹ B - C(T_max) ≥ 0 ∎
Rounding direction: All divisions use Rust integer truncation (rounds toward zero / floor for positive values), which always rounds down in favour of the contract. This means the contract never charges for a fractional second it has not earned.
Overflow protection: All arithmetic uses saturating_mul and saturating_sub, which clamp to i128::MAX / i128::MIN rather than wrapping. The max(0) clamp in calculate_remaining_balance provides a final safety net.
The following tests in contracts/utility_contracts/src/fuzz_tests.rs verify the invariant:
| Test | Description | Inputs |
|---|---|---|
test_stream_exhaustion_invariant_randomised |
100 000 randomised (balance, rate) pairs via deterministic LCG | balance ∈ [1, 10¹²], rate ∈ [1, 10⁶] |
test_stream_never_negative_after_pause_resume |
10-year simulation with pause/resume and partial top-ups | Fixed scenario, 315 M seconds |
test_rounding_always_favours_solvency |
Verifies floor-division rounding direction | Hand-crafted edge cases |
test_calculate_remaining_balance_never_negative |
Grid search over (balance, rate, elapsed) | 6 × 5 × 5 = 150 combinations including extremes |
All tests run on every Pull Request via the CI workflow (.github/workflows/test.yml).
- ✅ Single-stream balance exhaustion
- ✅ Pause / resume cycles
- ✅ Partial top-ups mid-stream
- ✅ Rounding-error accumulation over 10-year durations
- ✅ Overflow / underflow protection via saturating arithmetic
⚠️ Multi-stream interactions (covered by integration tests, not this invariant)⚠️ Oracle price conversion rounding (separate audit scope)
The formal invariant proof above satisfies the "High Assurance" requirement for institutional auditors. The deterministic fuzz harness (test_stream_exhaustion_invariant_randomised) can be reproduced exactly by any auditor by running:
cargo test -p utility_contracts test_stream_exhaustion_invariant_randomised -- --nocapture- Rent is only deducted when the contract TTL falls below a 6-month safety threshold (~3 110 400 ledgers).
- Deduction is capped at 1 000 stroops (0.0001 XLM) per claim.
- For non-XLM tokens the deduction is skipped silently to avoid blocking the stream.
- A
RentRenewevent is emitted with the deduction amount and new TTL for auditability.
- Fleet-level configuration changes require a 48-hour staging window.
- The Fleet Security Council (3-of-5 multi-sig) can veto any staged update within the window.
- Emergency circuit-breaker updates bypass the staging window.
- Lost council keys can be rotated by the DAO after a 7-day delay.
- All staged and vetoed events are emitted on-ledger for public transparency.
- The green energy ratio and credit multiplier must be set by the provider (acting as the whitelisted environmental auditor).
- Credits accumulate as fractional slices; only full integer credits trigger a cross-contract mint.
- If the minting contract is paused or has hit its issuance cap, pending credits are stored in a
Deferred_Issuancebuffer and can be retried later. - No fractional "dust" is lost: every stroop of green usage is counted in the accumulator.