529 lines
17 KiB
Go
529 lines
17 KiB
Go
package native
|
|
|
|
import (
|
|
"errors"
|
|
"math/big"
|
|
|
|
"github.com/tutus-one/tutus-chain/pkg/core/dao"
|
|
"github.com/tutus-one/tutus-chain/pkg/core/storage"
|
|
"github.com/tutus-one/tutus-chain/pkg/util"
|
|
)
|
|
|
|
// ARCH-003: Formal Verification Invariants
|
|
// This file documents critical system invariants that must hold at all times.
|
|
// These invariants serve multiple purposes:
|
|
// 1. Runtime verification during testing and canary deployments
|
|
// 2. Documentation for formal verification tools (TLA+, Coq, etc.)
|
|
// 3. Post-deployment monitoring and alerting
|
|
|
|
// InvariantCategory categorizes invariants by domain.
|
|
type InvariantCategory uint8
|
|
|
|
const (
|
|
InvariantCategoryToken InvariantCategory = iota
|
|
InvariantCategoryIdentity
|
|
InvariantCategoryGovernance
|
|
InvariantCategoryEconomic
|
|
InvariantCategorySecurity
|
|
InvariantCategoryCrossContract
|
|
)
|
|
|
|
// InvariantSeverity indicates the impact of violation.
|
|
type InvariantSeverity uint8
|
|
|
|
const (
|
|
// InvariantSeverityCritical means system halt required
|
|
InvariantSeverityCritical InvariantSeverity = iota
|
|
// InvariantSeverityHigh means immediate investigation required
|
|
InvariantSeverityHigh
|
|
// InvariantSeverityMedium means potential issue to investigate
|
|
InvariantSeverityMedium
|
|
// InvariantSeverityLow means informational anomaly
|
|
InvariantSeverityLow
|
|
)
|
|
|
|
// Invariant represents a system invariant that must hold.
|
|
type Invariant struct {
|
|
ID string
|
|
Name string
|
|
Description string
|
|
Category InvariantCategory
|
|
Severity InvariantSeverity
|
|
// FormalSpec is TLA+/Coq-style formal specification
|
|
FormalSpec string
|
|
}
|
|
|
|
// InvariantViolation records a violation of a system invariant.
|
|
type InvariantViolation struct {
|
|
InvariantID string
|
|
BlockHeight uint32
|
|
Details string
|
|
ActualValue string
|
|
ExpectedSpec string
|
|
}
|
|
|
|
// Invariant violations are critical errors.
|
|
var (
|
|
ErrInvariantViolation = errors.New("invariant violation detected")
|
|
ErrTokenSupplyMismatch = errors.New("token supply invariant violated")
|
|
ErrVitaUniqueness = errors.New("vita uniqueness invariant violated")
|
|
ErrRightsConsistency = errors.New("rights consistency invariant violated")
|
|
ErrBalanceNonNegative = errors.New("balance non-negativity invariant violated")
|
|
ErrCrossContractConsistency = errors.New("cross-contract consistency invariant violated")
|
|
)
|
|
|
|
// CriticalInvariants defines all system invariants that must always hold.
|
|
var CriticalInvariants = []Invariant{
|
|
// ============================================
|
|
// TOKEN INVARIANTS
|
|
// ============================================
|
|
{
|
|
ID: "TOK-001",
|
|
Name: "VTS Total Supply Conservation",
|
|
Description: "Sum of all VTS balances must equal total supply minus burned amount",
|
|
Category: InvariantCategoryToken,
|
|
Severity: InvariantSeverityCritical,
|
|
FormalSpec: `
|
|
INVARIANT VTSSupplyConservation ==
|
|
\A state \in ValidStates:
|
|
Sum({state.vts.balance[addr] : addr \in DOMAIN state.vts.balance})
|
|
= state.vts.totalSupply - state.vts.burnedAmount
|
|
`,
|
|
},
|
|
{
|
|
ID: "TOK-002",
|
|
Name: "Non-Negative Balances",
|
|
Description: "No token balance can ever be negative",
|
|
Category: InvariantCategoryToken,
|
|
Severity: InvariantSeverityCritical,
|
|
FormalSpec: `
|
|
INVARIANT NonNegativeBalances ==
|
|
\A state \in ValidStates:
|
|
\A addr \in DOMAIN state.vts.balance:
|
|
state.vts.balance[addr] >= 0
|
|
`,
|
|
},
|
|
{
|
|
ID: "TOK-003",
|
|
Name: "Lub Total Supply Conservation",
|
|
Description: "Lub supply follows predictable generation schedule",
|
|
Category: InvariantCategoryToken,
|
|
Severity: InvariantSeverityCritical,
|
|
FormalSpec: `
|
|
INVARIANT LubSupplyConservation ==
|
|
\A state \in ValidStates:
|
|
state.lub.totalSupply <= MaxLubSupply
|
|
/\ Sum({state.lub.balance[addr] : addr \in DOMAIN state.lub.balance})
|
|
= state.lub.totalSupply
|
|
`,
|
|
},
|
|
|
|
// ============================================
|
|
// IDENTITY INVARIANTS
|
|
// ============================================
|
|
{
|
|
ID: "IDN-001",
|
|
Name: "Vita Uniqueness Per Person",
|
|
Description: "Each natural person can hold at most one Vita token globally",
|
|
Category: InvariantCategoryIdentity,
|
|
Severity: InvariantSeverityCritical,
|
|
FormalSpec: `
|
|
INVARIANT VitaUniqueness ==
|
|
\A state \in ValidStates:
|
|
\A p1, p2 \in state.vita.tokens:
|
|
p1.biometricHash = p2.biometricHash => p1.tokenID = p2.tokenID
|
|
`,
|
|
},
|
|
{
|
|
ID: "IDN-002",
|
|
Name: "Vita Non-Transferability",
|
|
Description: "Vita tokens cannot be transferred except through death/recovery",
|
|
Category: InvariantCategoryIdentity,
|
|
Severity: InvariantSeverityCritical,
|
|
FormalSpec: `
|
|
INVARIANT VitaNonTransferable ==
|
|
\A state, state' \in ValidStates:
|
|
\A vita \in state.vita.tokens:
|
|
state'.vita.tokens[vita.tokenID].owner # vita.owner
|
|
=> state'.vita.tokens[vita.tokenID].status \in {Suspended, Revoked}
|
|
\/ vita.owner.status = Deceased
|
|
`,
|
|
},
|
|
{
|
|
ID: "IDN-003",
|
|
Name: "Vita Count Equals Active Citizens",
|
|
Description: "Active Vita count must match registered citizen count",
|
|
Category: InvariantCategoryIdentity,
|
|
Severity: InvariantSeverityHigh,
|
|
FormalSpec: `
|
|
INVARIANT VitaCountConsistency ==
|
|
\A state \in ValidStates:
|
|
Cardinality({v \in state.vita.tokens : v.status = Active})
|
|
= state.vita.activeCount
|
|
`,
|
|
},
|
|
|
|
// ============================================
|
|
// GOVERNANCE INVARIANTS
|
|
// ============================================
|
|
{
|
|
ID: "GOV-001",
|
|
Name: "One Person One Vote",
|
|
Description: "Each Vita holder can cast at most one vote per proposal",
|
|
Category: InvariantCategoryGovernance,
|
|
Severity: InvariantSeverityCritical,
|
|
FormalSpec: `
|
|
INVARIANT OnePersonOneVote ==
|
|
\A state \in ValidStates:
|
|
\A p \in state.eligere.proposals:
|
|
\A v \in state.vita.tokens:
|
|
Cardinality({vote \in p.votes : vote.vitaID = v.tokenID}) <= 1
|
|
`,
|
|
},
|
|
{
|
|
ID: "GOV-002",
|
|
Name: "Voting Age Enforcement",
|
|
Description: "Only Vita holders >= voting age can vote",
|
|
Category: InvariantCategoryGovernance,
|
|
Severity: InvariantSeverityHigh,
|
|
FormalSpec: `
|
|
INVARIANT VotingAgeEnforced ==
|
|
\A state \in ValidStates:
|
|
\A vote \in AllVotes(state):
|
|
AgeOf(vote.vitaID, state.currentBlock) >= state.config.votingAge
|
|
`,
|
|
},
|
|
{
|
|
ID: "GOV-003",
|
|
Name: "Committee Authority Separation",
|
|
Description: "Domain committees have authority only within their domain",
|
|
Category: InvariantCategoryGovernance,
|
|
Severity: InvariantSeverityHigh,
|
|
FormalSpec: `
|
|
INVARIANT CommitteeAuthoritySeparation ==
|
|
\A state \in ValidStates:
|
|
\A action \in state.actions:
|
|
action.requiredDomain = DomainHealth
|
|
=> action.authorizer \in state.committees.health
|
|
`,
|
|
},
|
|
|
|
// ============================================
|
|
// ECONOMIC INVARIANTS
|
|
// ============================================
|
|
{
|
|
ID: "ECO-001",
|
|
Name: "Tribute Conservation",
|
|
Description: "Total tribute collected equals sum of redistributions plus treasury",
|
|
Category: InvariantCategoryEconomic,
|
|
Severity: InvariantSeverityHigh,
|
|
FormalSpec: `
|
|
INVARIANT TributeConservation ==
|
|
\A state \in ValidStates:
|
|
state.tribute.totalCollected
|
|
= state.tribute.totalRedistributed + state.treasury.tributeBalance
|
|
`,
|
|
},
|
|
{
|
|
ID: "ECO-002",
|
|
Name: "Investment Opportunity Bounds",
|
|
Description: "Investment totals cannot exceed opportunity limits",
|
|
Category: InvariantCategoryEconomic,
|
|
Severity: InvariantSeverityHigh,
|
|
FormalSpec: `
|
|
INVARIANT InvestmentBounds ==
|
|
\A state \in ValidStates:
|
|
\A opp \in state.collocatio.opportunities:
|
|
Sum({inv.amount : inv \in opp.investments}) <= opp.maxAmount
|
|
`,
|
|
},
|
|
|
|
// ============================================
|
|
// SECURITY INVARIANTS
|
|
// ============================================
|
|
{
|
|
ID: "SEC-001",
|
|
Name: "Rights Restriction Requires Due Process",
|
|
Description: "Rights can only be restricted with valid judicial order",
|
|
Category: InvariantCategorySecurity,
|
|
Severity: InvariantSeverityCritical,
|
|
FormalSpec: `
|
|
INVARIANT RightsRestrictionDueProcess ==
|
|
\A state \in ValidStates:
|
|
\A restriction \in state.lex.restrictions:
|
|
restriction.caseID # ""
|
|
/\ restriction.authorizedBy \in state.roles.judges
|
|
/\ restriction.expiresAt > state.currentBlock
|
|
`,
|
|
},
|
|
{
|
|
ID: "SEC-002",
|
|
Name: "Role Expiry Enforcement",
|
|
Description: "Expired roles grant no permissions",
|
|
Category: InvariantCategorySecurity,
|
|
Severity: InvariantSeverityHigh,
|
|
FormalSpec: `
|
|
INVARIANT ExpiredRolesInactive ==
|
|
\A state \in ValidStates:
|
|
\A role \in state.roleRegistry.assignments:
|
|
role.expiresAt <= state.currentBlock
|
|
=> ~HasPermission(role.holder, role.roleID, state)
|
|
`,
|
|
},
|
|
{
|
|
ID: "SEC-003",
|
|
Name: "Circuit Breaker Effectiveness",
|
|
Description: "Open circuit breakers block all protected operations",
|
|
Category: InvariantCategorySecurity,
|
|
Severity: InvariantSeverityHigh,
|
|
FormalSpec: `
|
|
INVARIANT CircuitBreakerEffective ==
|
|
\A state \in ValidStates:
|
|
\A breaker \in state.circuitBreakers:
|
|
breaker.state = Open
|
|
=> ~\E op \in state.operations:
|
|
op.protected = breaker.name /\ op.status = Completed
|
|
`,
|
|
},
|
|
|
|
// ============================================
|
|
// CROSS-CONTRACT INVARIANTS
|
|
// ============================================
|
|
{
|
|
ID: "XCT-001",
|
|
Name: "Annos-Vita Consistency",
|
|
Description: "Every Annos lifespan record has corresponding Vita token",
|
|
Category: InvariantCategoryCrossContract,
|
|
Severity: InvariantSeverityHigh,
|
|
FormalSpec: `
|
|
INVARIANT AnnosVitaConsistency ==
|
|
\A state \in ValidStates:
|
|
\A record \in state.annos.lifespans:
|
|
\E vita \in state.vita.tokens:
|
|
vita.tokenID = record.vitaID
|
|
`,
|
|
},
|
|
{
|
|
ID: "XCT-002",
|
|
Name: "Scire-Vita Consistency",
|
|
Description: "Education accounts require valid Vita holders",
|
|
Category: InvariantCategoryCrossContract,
|
|
Severity: InvariantSeverityHigh,
|
|
FormalSpec: `
|
|
INVARIANT ScireVitaConsistency ==
|
|
\A state \in ValidStates:
|
|
\A account \in state.scire.accounts:
|
|
\E vita \in state.vita.tokens:
|
|
vita.tokenID = account.vitaID /\ vita.status = Active
|
|
`,
|
|
},
|
|
{
|
|
ID: "XCT-003",
|
|
Name: "Salus-Vita Consistency",
|
|
Description: "Healthcare accounts require valid Vita holders",
|
|
Category: InvariantCategoryCrossContract,
|
|
Severity: InvariantSeverityHigh,
|
|
FormalSpec: `
|
|
INVARIANT SalusVitaConsistency ==
|
|
\A state \in ValidStates:
|
|
\A account \in state.salus.accounts:
|
|
\E vita \in state.vita.tokens:
|
|
vita.tokenID = account.vitaID
|
|
`,
|
|
},
|
|
{
|
|
ID: "XCT-004",
|
|
Name: "Federation Debt Balance",
|
|
Description: "Inter-chain debts sum to zero globally",
|
|
Category: InvariantCategoryCrossContract,
|
|
Severity: InvariantSeverityHigh,
|
|
FormalSpec: `
|
|
INVARIANT FederationDebtBalance ==
|
|
\A globalState \in ValidGlobalStates:
|
|
Sum({chain.federation.debt[other] :
|
|
chain \in globalState.chains,
|
|
other \in globalState.chains})
|
|
= 0
|
|
`,
|
|
},
|
|
}
|
|
|
|
// InvariantChecker provides runtime invariant verification.
|
|
type InvariantChecker struct {
|
|
contractID int32
|
|
violations []InvariantViolation
|
|
}
|
|
|
|
// NewInvariantChecker creates a new invariant checker.
|
|
func NewInvariantChecker(contractID int32) *InvariantChecker {
|
|
return &InvariantChecker{
|
|
contractID: contractID,
|
|
violations: make([]InvariantViolation, 0),
|
|
}
|
|
}
|
|
|
|
// CheckVTSSupplyInvariant verifies VTS supply conservation (TOK-001).
|
|
func (ic *InvariantChecker) CheckVTSSupplyInvariant(d *dao.Simple, vtsContractID int32) error {
|
|
// Get total supply
|
|
supplyKey := []byte{0x11} // VTS total supply prefix
|
|
supplyData := d.GetStorageItem(vtsContractID, supplyKey)
|
|
if supplyData == nil {
|
|
return nil // Not initialized
|
|
}
|
|
totalSupply := new(big.Int).SetBytes(supplyData)
|
|
|
|
// Sum all balances
|
|
balanceSum := big.NewInt(0)
|
|
balancePrefix := []byte{0x14} // VTS balance prefix
|
|
|
|
d.Seek(vtsContractID, storage.SeekRange{Prefix: balancePrefix}, func(k, v []byte) bool {
|
|
balance := new(big.Int).SetBytes(v)
|
|
balanceSum.Add(balanceSum, balance)
|
|
return true
|
|
})
|
|
|
|
if totalSupply.Cmp(balanceSum) != 0 {
|
|
ic.recordViolation("TOK-001", 0, "Supply mismatch",
|
|
balanceSum.String(), totalSupply.String())
|
|
return ErrTokenSupplyMismatch
|
|
}
|
|
|
|
return nil
|
|
}
|
|
|
|
// CheckVitaUniquenessInvariant verifies Vita uniqueness (IDN-001).
|
|
func (ic *InvariantChecker) CheckVitaUniquenessInvariant(d *dao.Simple, vitaContractID int32) error {
|
|
biometricHashes := make(map[util.Uint256]uint64)
|
|
tokenPrefix := []byte{0x01} // Vita token prefix
|
|
|
|
var violation bool
|
|
d.Seek(vitaContractID, storage.SeekRange{Prefix: tokenPrefix}, func(k, v []byte) bool {
|
|
if len(v) < 32 {
|
|
return true
|
|
}
|
|
// Extract biometric hash from token data
|
|
var bioHash util.Uint256
|
|
copy(bioHash[:], v[:32])
|
|
|
|
if existingID, exists := biometricHashes[bioHash]; exists {
|
|
ic.recordViolation("IDN-001", 0, "Duplicate biometric hash",
|
|
"Multiple tokens", "Single token per biometric")
|
|
_ = existingID // Reference to suppress unused warning
|
|
violation = true
|
|
return false
|
|
}
|
|
|
|
// Extract token ID from key
|
|
if len(k) >= 8 {
|
|
tokenID := uint64(k[0])<<56 | uint64(k[1])<<48 | uint64(k[2])<<40 |
|
|
uint64(k[3])<<32 | uint64(k[4])<<24 | uint64(k[5])<<16 |
|
|
uint64(k[6])<<8 | uint64(k[7])
|
|
biometricHashes[bioHash] = tokenID
|
|
}
|
|
return true
|
|
})
|
|
|
|
if violation {
|
|
return ErrVitaUniqueness
|
|
}
|
|
return nil
|
|
}
|
|
|
|
// CheckNonNegativeBalances verifies no negative balances exist (TOK-002).
|
|
func (ic *InvariantChecker) CheckNonNegativeBalances(d *dao.Simple, contractID int32, balancePrefix byte) error {
|
|
prefix := []byte{balancePrefix}
|
|
|
|
var violation bool
|
|
d.Seek(contractID, storage.SeekRange{Prefix: prefix}, func(k, v []byte) bool {
|
|
balance := new(big.Int).SetBytes(v)
|
|
if balance.Sign() < 0 {
|
|
ic.recordViolation("TOK-002", 0, "Negative balance detected",
|
|
balance.String(), ">= 0")
|
|
violation = true
|
|
return false
|
|
}
|
|
return true
|
|
})
|
|
|
|
if violation {
|
|
return ErrBalanceNonNegative
|
|
}
|
|
return nil
|
|
}
|
|
|
|
// CheckRightsConsistency verifies rights restrictions have valid due process (SEC-001).
|
|
func (ic *InvariantChecker) CheckRightsConsistency(d *dao.Simple, lexContractID int32, currentBlock uint32) error {
|
|
restrictionPrefix := []byte{0x20} // Lex restriction prefix
|
|
|
|
var violation bool
|
|
d.Seek(lexContractID, storage.SeekRange{Prefix: restrictionPrefix}, func(k, v []byte) bool {
|
|
if len(v) < 40 {
|
|
return true
|
|
}
|
|
|
|
// Check if restriction has case ID (non-empty)
|
|
caseIDLen := v[0]
|
|
if caseIDLen == 0 {
|
|
ic.recordViolation("SEC-001", currentBlock,
|
|
"Rights restriction without case ID", "empty", "non-empty case ID")
|
|
violation = true
|
|
return false
|
|
}
|
|
|
|
return true
|
|
})
|
|
|
|
if violation {
|
|
return ErrRightsConsistency
|
|
}
|
|
return nil
|
|
}
|
|
|
|
// recordViolation records an invariant violation.
|
|
func (ic *InvariantChecker) recordViolation(invariantID string, blockHeight uint32, details, actual, expected string) {
|
|
ic.violations = append(ic.violations, InvariantViolation{
|
|
InvariantID: invariantID,
|
|
BlockHeight: blockHeight,
|
|
Details: details,
|
|
ActualValue: actual,
|
|
ExpectedSpec: expected,
|
|
})
|
|
}
|
|
|
|
// GetViolations returns all recorded violations.
|
|
func (ic *InvariantChecker) GetViolations() []InvariantViolation {
|
|
return ic.violations
|
|
}
|
|
|
|
// ClearViolations clears recorded violations.
|
|
func (ic *InvariantChecker) ClearViolations() {
|
|
ic.violations = make([]InvariantViolation, 0)
|
|
}
|
|
|
|
// RunAllCriticalChecks runs all critical invariant checks.
|
|
func (ic *InvariantChecker) RunAllCriticalChecks(d *dao.Simple, contracts ContractIDs, currentBlock uint32) []InvariantViolation {
|
|
ic.ClearViolations()
|
|
|
|
// Run critical checks
|
|
_ = ic.CheckVTSSupplyInvariant(d, contracts.VTS)
|
|
_ = ic.CheckVitaUniquenessInvariant(d, contracts.Vita)
|
|
_ = ic.CheckNonNegativeBalances(d, contracts.VTS, 0x14)
|
|
_ = ic.CheckNonNegativeBalances(d, contracts.Tutus, 0x14)
|
|
_ = ic.CheckNonNegativeBalances(d, contracts.Lub, 0x14)
|
|
_ = ic.CheckRightsConsistency(d, contracts.Lex, currentBlock)
|
|
|
|
return ic.GetViolations()
|
|
}
|
|
|
|
// ContractIDs holds contract identifiers for invariant checking.
|
|
type ContractIDs struct {
|
|
VTS int32
|
|
Vita int32
|
|
Tutus int32
|
|
Lub int32
|
|
Lex int32
|
|
Annos int32
|
|
Scire int32
|
|
Salus int32
|
|
}
|