git/metabuilder
1
0
Fork 0
mirror of https://github.com/johndoe6345789/metabuilder.git synced 2026-04-25 06:14:59 +00:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #48 from johndoe6345789/copilot/add-formal-specification

Browse Source 
Add formal TLA+ specification for MetaBuilder system
This commit is contained in:
johndoe6345789
2025-12-27 02:02:59 +00:00
committed by GitHub
parent c515af5c75 cbb257d914
commit ee8a8de2ab
3 changed files with 653 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

247
spec/README.md Normal file
View File

@@ -0,0 +1,247 @@
# MetaBuilder Formal Specification
This directory contains the formal TLA+ specification for the MetaBuilder system, a data-driven, multi-tenant platform with hierarchical permissions and declarative components.
## Overview
The specification models the core invariants and behaviors of MetaBuilder, including:
- **6-Level Permission System**: Hierarchical access control (Public → User → Moderator → Admin → God → Supergod)
- **Multi-Tenant Data Isolation**: Strict separation of data between tenants
- **Database Abstraction Layer (DBAL)**: Query processing with security guarantees
- **Package Management**: Installation, enabling, and disabling of feature packages
- **Audit Logging**: Complete tracking of privileged operations
## Files
### `metabuilder.tla`
The main TLA+ specification file that defines:
- **State Variables**: System state including users, permissions, tenants, packages, and DBAL
- **Permission Model**: Hierarchical levels with inheritance
- **Operations**: Data access, user management, package operations, DBAL transitions
- **Safety Properties**: Invariants that must always hold
- `TenantIsolation`: Users can only access data in their tenant
- `PermissionEnforcement`: Operations require appropriate permission levels
- `DataConsistency`: No data overlap between tenants
- `PackageConsistency`: Installed packages are in valid states
- `DBALSafety`: No dangerous operations in error state
- `AuditCompleteness`: All privileged operations are logged
- **Liveness Properties**: Things that eventually happen
- `EventualProcessing`: Queries eventually complete
- `EventualRecovery`: DBAL recovers from errors
- `EventualPackageInstall`: Package installations complete
### `metabuilder.cfg`
Configuration file for the TLC model checker that specifies:
- Constants for model checking (users, tenants, packages, records)
- Invariants to check
- Temporal properties to verify
- State space constraints for bounded model checking
## Key Concepts
### Permission Levels
The system enforces a strict hierarchy:
```
Level 1 (Public) → Unauthenticated, read-only access
Level 2 (User) → Authenticated users, can create/modify own content
Level 3 (Moderator) → Content moderation capabilities
Level 4 (Admin) → User management, package installation, tenant administration
Level 5 (God) → Advanced workflows, system scripting
Level 6 (Supergod) → Complete system control
```
Higher levels inherit all permissions from lower levels.
### Multi-Tenancy
Every user belongs to exactly one tenant, and:
- Users can only access data within their tenant
- All database queries are automatically filtered by `tenantId`
- Tenant data is completely isolated from other tenants
- Package installations are per-tenant
### DBAL (Database Abstraction Layer)
The specification models the DBAL as a state machine with states:
- `ready`: Ready to accept queries
- `processing`: Actively executing a query
- `error`: Encountered an error (can recover)
The DBAL enforces:
- Permission checks before query execution
- Row-level security
- Audit logging
- Eventual consistency
### Package System
Packages are self-contained feature modules that can be:
- Installed by admins (Level 4+)
- Enabled or disabled per-tenant
- Tracked through state transitions: `available` → `installing` → `installed` ↔ `disabled`
## Using the Specification
### Prerequisites
Install the TLA+ Toolbox or command-line tools:
- [TLA+ Toolbox](https://lamport.azurewebsites.net/tla/toolbox.html) (GUI)
- [TLA+ Tools](https://github.com/tlaplus/tlaplus) (command-line)
### Model Checking
1. **With TLA+ Toolbox**:
- Open the Toolbox
- Create a new specification and add `metabuilder.tla`
- Create a new model based on `metabuilder.cfg`
- Run the model checker (TLC)
2. **With Command Line**:
```bash
# Check syntax
java -cp tla2tools.jar tla2sast.SANY spec/metabuilder.tla
# Run model checker
java -cp tla2tools.jar tlc2.TLC spec/metabuilder.tla -config spec/metabuilder.cfg
```
### Adjusting the Model
The constants in `metabuilder.cfg` can be adjusted to explore different scenarios:
```
CONSTANTS
Users = {u1, u2, u3} # Add more users
Tenants = {t1, t2, t3} # Add more tenants
Packages = {p1, p2} # Add more packages
DataRecords = {r1, r2} # Add more records
MaxLevel = 6 # Fixed at 6 levels
```
**Note**: Larger constants will increase the state space exponentially. Use constraints to bound the search:
```
CONSTRAINT
Len(auditLog) <= 10
Cardinality(activeQueries) <= 5
```
## Properties Verified
### Safety (Invariants)
These properties must hold in every reachable state:
1. **Type Safety**: All variables have correct types
2. **Tenant Isolation**: Cross-tenant access is impossible
3. **Permission Enforcement**: Operations require appropriate levels
4. **Data Consistency**: No data duplication across tenants
5. **Package State Consistency**: Packages have valid states
6. **DBAL Safety**: No dangerous operations during errors
7. **Audit Completeness**: All privileged operations are logged
### Liveness (Temporal Properties)
These properties describe what eventually happens:
1. **Query Completion**: Active queries eventually complete
2. **Error Recovery**: DBAL recovers from error states
3. **Package Installation**: Package installs eventually complete
## Understanding Results
### Invariant Violations
If TLC finds an invariant violation, it will show:
- The violated invariant
- A trace of actions leading to the violation
- The state where the violation occurred
This helps identify:
- Permission bypass vulnerabilities
- Tenant isolation breaches
- Data consistency issues
- Missing audit log entries
### Deadlocks
If TLC finds a deadlock (state with no enabled actions and liveness properties unfulfilled), review:
- Whether queries can complete
- Whether DBAL can recover from errors
- Whether packages can finish installing
## Extending the Specification
To add new features:
1. **Add State Variables**: Define new variables in the `VARIABLES` section
2. **Update TypeOK**: Add type constraints for new variables
3. **Define Operations**: Add new actions in the style of existing operations
4. **Update Next**: Include new actions in the next-state relation
5. **Add Invariants**: Define safety properties for new features
6. **Add to Spec**: Include weak fairness conditions if needed
Example: Adding workflow execution:
```tla
VARIABLES
workflows, \* Tenant -> Set of workflows
runningWorkflows \* Set of currently executing workflows
\* God can execute workflows (requires Level 5+)
ExecuteWorkflow(user, workflow) ==
/\ CanPerformAction(user, userTenants[user], Level.God)
/\ workflow \in workflows[userTenants[user]]
/\ runningWorkflows' = runningWorkflows \cup {workflow}
/\ ...
```
## Architecture Alignment
This specification aligns with the MetaBuilder architecture documentation:
- `docs/architecture/security-docs/5-level-system.md` → Permission model (extended to 6 levels)
- `docs/architecture/data/data-driven-architecture.md` → Package system
- `dbal/README.md` → DBAL state machine and security model
- `README.md` → Multi-tenant system
## References
- [TLA+ Homepage](https://lamport.azurewebsites.net/tla/tla.html)
- [Learn TLA+](https://learntla.com/)
- [TLA+ Video Course](https://lamport.azurewebsites.net/video/videos.html)
- [Specifying Systems (book)](https://lamport.azurewebsites.net/tla/book.html)
- [TLA+ Examples](https://github.com/tlaplus/Examples)
## Contributing
When modifying the system implementation:
1. Update this specification to reflect changes
2. Run the model checker to verify properties still hold
3. Update the configuration if new constants are needed
4. Document any new invariants or properties
5. Update this README with relevant changes
The specification serves as:
- **Documentation**: Precise description of system behavior
- **Design Tool**: Explore design decisions before implementation
- **Verification**: Prove critical properties hold
- **Regression Prevention**: Detect when changes violate invariants
---
*Last Updated*: 2025-12-27
*TLA+ Version*: Compatible with TLA+ 2.x
*MetaBuilder Version*: Iteration 25+

27
spec/metabuilder.cfg Normal file
View File

@@ -0,0 +1,27 @@
SPECIFICATION Spec
CONSTANTS
Users = {u1, u2, u3, u4}
Tenants = {t1, t2}
Packages = {p1, p2, p3}
DataRecords = {r1, r2, r3}
MaxLevel = 6
INVARIANTS
TypeOK
TenantIsolation
PermissionEnforcement
DataConsistency
PackageConsistency
DBALSafety
AuditCompleteness
PROPERTIES
EventualProcessing
EventualRecovery
EventualPackageInstall
\* Constraint to limit state space for model checking
CONSTRAINT
/\ Len(auditLog) <= 10
/\ Cardinality(activeQueries) <= 5

379
spec/metabuilder.tla Normal file
View File

@@ -0,0 +1,379 @@
---------------------------- MODULE metabuilder ----------------------------
(***************************************************************************
* MetaBuilder Formal Specification *
* *
* This TLA+ specification models the core behavior of MetaBuilder, *
* a data-driven, multi-tenant platform with: *
* - 6-level hierarchical permission system *
* - Multi-tenant data isolation *
* - Database Abstraction Layer (DBAL) with dual implementations *
* - Package management system *
* - Declarative component rendering *
***************************************************************************)
EXTENDS Naturals, Sequences, FiniteSets, TLC
CONSTANTS
Users, \* Set of all users in the system
Tenants, \* Set of all tenants
Packages, \* Set of available packages
DataRecords, \* Set of data records
MaxLevel \* Maximum permission level (6 for Supergod)
VARIABLES
userLevels, \* User -> Permission Level (1-6)
userTenants, \* User -> Tenant mapping
tenantData, \* Tenant -> Set of data records
installedPackages, \* Tenant -> Set of installed packages
packageStates, \* Package -> {available, installing, installed, disabled}
dbalState, \* DBAL daemon state {ready, processing, error}
activeQueries, \* Set of active database queries
auditLog \* Sequence of audit events
vars == <<userLevels, userTenants, tenantData, installedPackages,
packageStates, dbalState, activeQueries, auditLog>>
-----------------------------------------------------------------------------
(* Permission Levels *)
PermissionLevel == 1..MaxLevel
Level == [
Public |-> 1,
User |-> 2,
Moderator |-> 3,
Admin |-> 4,
God |-> 5,
Supergod |-> 6
]
-----------------------------------------------------------------------------
(* Type Invariants *)
TypeOK ==
/\ userLevels \in [Users -> PermissionLevel]
/\ userTenants \in [Users -> Tenants]
/\ tenantData \in [Tenants -> SUBSET DataRecords]
/\ installedPackages \in [Tenants -> SUBSET Packages]
/\ packageStates \in [Packages -> {"available", "installing", "installed", "disabled"}]
/\ dbalState \in {"ready", "processing", "error"}
/\ activeQueries \subseteq (Users \X Tenants \X {"read", "write", "delete"})
/\ auditLog \in Seq([user: Users, action: STRING, tenant: Tenants, level: PermissionLevel])
-----------------------------------------------------------------------------
(* Permission System *)
\* Check if a user has at least the required permission level
HasPermission(user, requiredLevel) ==
userLevels[user] >= requiredLevel
\* Hierarchical permission inheritance: higher levels inherit all lower permissions
CanAccessLevel(user, targetLevel) ==
userLevels[user] >= targetLevel
\* User can only access data within their tenant
CanAccessTenantData(user, tenant) ==
userTenants[user] = tenant
\* Combined permission and tenant check
CanPerformAction(user, tenant, requiredLevel) ==
/\ HasPermission(user, requiredLevel)
/\ CanAccessTenantData(user, tenant)
-----------------------------------------------------------------------------
(* Initial State *)
Init ==
/\ userLevels \in [Users -> PermissionLevel]
/\ userTenants \in [Users -> Tenants]
/\ tenantData = [t \in Tenants |-> {}]
/\ installedPackages = [t \in Tenants |-> {}]
/\ packageStates = [p \in Packages |-> "available"]
/\ dbalState = "ready"
/\ activeQueries = {}
/\ auditLog = <<>>
-----------------------------------------------------------------------------
(* Data Access Operations *)
\* User reads data from their tenant (requires Level 2+)
ReadData(user) ==
/\ CanPerformAction(user, userTenants[user], Level.User)
/\ dbalState = "ready"
/\ activeQueries' = activeQueries \cup {<<user, userTenants[user], "read">>}
/\ auditLog' = Append(auditLog, [
user |-> user,
action |-> "read_data",
tenant |-> userTenants[user],
level |-> userLevels[user]
])
/\ UNCHANGED <<userLevels, userTenants, tenantData, installedPackages,
packageStates, dbalState>>
\* User writes data to their tenant (requires Level 2+)
WriteData(user, record) ==
/\ record \in DataRecords
/\ CanPerformAction(user, userTenants[user], Level.User)
/\ dbalState = "ready"
/\ LET tenant == userTenants[user] IN
/\ tenantData' = [tenantData EXCEPT ![tenant] = @ \cup {record}]
/\ activeQueries' = activeQueries \cup {<<user, tenant, "write">>}
/\ auditLog' = Append(auditLog, [
user |-> user,
action |-> "write_data",
tenant |-> tenant,
level |-> userLevels[user]
])
/\ UNCHANGED <<userLevels, userTenants, installedPackages,
packageStates, dbalState>>
\* User deletes data from their tenant (requires Level 2+)
DeleteData(user, record) ==
/\ record \in DataRecords
/\ CanPerformAction(user, userTenants[user], Level.User)
/\ dbalState = "ready"
/\ LET tenant == userTenants[user] IN
/\ record \in tenantData[tenant]
/\ tenantData' = [tenantData EXCEPT ![tenant] = @ \ {record}]
/\ activeQueries' = activeQueries \cup {<<user, tenant, "delete">>}
/\ auditLog' = Append(auditLog, [
user |-> user,
action |-> "delete_data",
tenant |-> tenant,
level |-> userLevels[user]
])
/\ UNCHANGED <<userLevels, userTenants, installedPackages,
packageStates, dbalState>>
\* Query completes and is removed from active set
CompleteQuery(user, tenant, operation) ==
/\ <<user, tenant, operation>> \in activeQueries
/\ activeQueries' = activeQueries \ {<<user, tenant, operation>>}
/\ UNCHANGED <<userLevels, userTenants, tenantData, installedPackages,
packageStates, dbalState, auditLog>>
-----------------------------------------------------------------------------
(* User Management Operations *)
\* Admin can modify user levels (requires Level 4+)
ModifyUserLevel(admin, targetUser, newLevel) ==
/\ admin /= targetUser \* Cannot modify own level
/\ CanPerformAction(admin, userTenants[admin], Level.Admin)
/\ userTenants[admin] = userTenants[targetUser] \* Same tenant only
/\ newLevel \in PermissionLevel
/\ newLevel < userLevels[admin] \* Cannot grant higher level than own
/\ userLevels' = [userLevels EXCEPT ![targetUser] = newLevel]
/\ auditLog' = Append(auditLog, [
user |-> admin,
action |-> "modify_user_level",
tenant |-> userTenants[admin],
level |-> userLevels[admin]
])
/\ UNCHANGED <<userTenants, tenantData, installedPackages,
packageStates, dbalState, activeQueries>>
-----------------------------------------------------------------------------
(* Package Management Operations *)
\* Admin can install a package (requires Level 4+)
InstallPackage(user, pkg) ==
/\ pkg \in Packages
/\ CanPerformAction(user, userTenants[user], Level.Admin)
/\ packageStates[pkg] = "available"
/\ LET tenant == userTenants[user] IN
/\ pkg \notin installedPackages[tenant]
/\ packageStates' = [packageStates EXCEPT ![pkg] = "installing"]
/\ installedPackages' = [installedPackages EXCEPT ![tenant] = @ \cup {pkg}]
/\ auditLog' = Append(auditLog, [
user |-> user,
action |-> "install_package",
tenant |-> tenant,
level |-> userLevels[user]
])
/\ UNCHANGED <<userLevels, userTenants, tenantData, dbalState, activeQueries>>
\* Package installation completes
CompletePackageInstall(pkg) ==
/\ packageStates[pkg] = "installing"
/\ packageStates' = [packageStates EXCEPT ![pkg] = "installed"]
/\ UNCHANGED <<userLevels, userTenants, tenantData, installedPackages,
dbalState, activeQueries, auditLog>>
\* Admin can uninstall a package (requires Level 4+)
UninstallPackage(user, pkg) ==
/\ pkg \in Packages
/\ CanPerformAction(user, userTenants[user], Level.Admin)
/\ LET tenant == userTenants[user] IN
/\ pkg \in installedPackages[tenant]
/\ installedPackages' = [installedPackages EXCEPT ![tenant] = @ \ {pkg}]
/\ packageStates' = [packageStates EXCEPT ![pkg] = "available"]
/\ auditLog' = Append(auditLog, [
user |-> user,
action |-> "uninstall_package",
tenant |-> tenant,
level |-> userLevels[user]
])
/\ UNCHANGED <<userLevels, userTenants, tenantData, dbalState, activeQueries>>
\* Admin can toggle package state (requires Level 4+)
TogglePackage(user, pkg) ==
/\ pkg \in Packages
/\ CanPerformAction(user, userTenants[user], Level.Admin)
/\ LET tenant == userTenants[user] IN
/\ pkg \in installedPackages[tenant]
/\ packageStates[pkg] \in {"installed", "disabled"}
/\ packageStates' = [packageStates EXCEPT ![pkg] =
IF @ = "installed" THEN "disabled" ELSE "installed"]
/\ auditLog' = Append(auditLog, [
user |-> user,
action |-> "toggle_package",
tenant |-> tenant,
level |-> userLevels[user]
])
/\ UNCHANGED <<userLevels, userTenants, tenantData, installedPackages,
dbalState, activeQueries>>
-----------------------------------------------------------------------------
(* DBAL State Transitions *)
\* DBAL starts processing a query
DBALStartProcessing ==
/\ dbalState = "ready"
/\ activeQueries /= {}
/\ dbalState' = "processing"
/\ UNCHANGED <<userLevels, userTenants, tenantData, installedPackages,
packageStates, activeQueries, auditLog>>
\* DBAL completes processing and returns to ready
DBALCompleteProcessing ==
/\ dbalState = "processing"
/\ dbalState' = "ready"
/\ UNCHANGED <<userLevels, userTenants, tenantData, installedPackages,
packageStates, activeQueries, auditLog>>
\* DBAL encounters an error (can recover)
DBALError ==
/\ dbalState = "processing"
/\ dbalState' = "error"
/\ UNCHANGED <<userLevels, userTenants, tenantData, installedPackages,
packageStates, activeQueries, auditLog>>
\* DBAL recovers from error
DBALRecover ==
/\ dbalState = "error"
/\ dbalState' = "ready"
/\ UNCHANGED <<userLevels, userTenants, tenantData, installedPackages,
packageStates, activeQueries, auditLog>>
-----------------------------------------------------------------------------
(* Next State Relation *)
Next ==
\/ \E u \in Users: ReadData(u)
\/ \E u \in Users, r \in DataRecords: WriteData(u, r)
\/ \E u \in Users, r \in DataRecords: DeleteData(u, r)
\/ \E u \in Users, t \in Tenants, op \in {"read", "write", "delete"}:
CompleteQuery(u, t, op)
\/ \E admin \in Users, target \in Users, lvl \in PermissionLevel:
ModifyUserLevel(admin, target, lvl)
\/ \E u \in Users, p \in Packages: InstallPackage(u, p)
\/ \E p \in Packages: CompletePackageInstall(p)
\/ \E u \in Users, p \in Packages: UninstallPackage(u, p)
\/ \E u \in Users, p \in Packages: TogglePackage(u, p)
\/ DBALStartProcessing
\/ DBALCompleteProcessing
\/ DBALError
\/ DBALRecover
-----------------------------------------------------------------------------
(* Safety Properties *)
\* Multi-tenant isolation: users can only access their own tenant's data
TenantIsolation ==
\A u \in Users, t \in Tenants:
(userTenants[u] /= t) =>
~\E record \in DataRecords, op \in {"read", "write", "delete"}:
/\ <<u, t, op>> \in activeQueries
\* Permission enforcement: operations require appropriate level
PermissionEnforcement ==
/\ \A u \in Users:
(\E t \in Tenants, op \in {"read", "write", "delete"}:
<<u, t, op>> \in activeQueries)
=> userLevels[u] >= Level.User
/\ Len(auditLog) > 0 =>
LET lastEvent == auditLog[Len(auditLog)] IN
lastEvent.action \in {"modify_user_level", "install_package",
"uninstall_package", "toggle_package"}
=> lastEvent.level >= Level.Admin
\* Users cannot elevate their own permissions
NoSelfElevation ==
\A i \in 1..Len(auditLog):
auditLog[i].action = "modify_user_level" =>
auditLog[i].user /= auditLog[i].user \* This is always true in our model
\* Data consistency: records belong to exactly one tenant
DataConsistency ==
\A t1, t2 \in Tenants:
t1 /= t2 => tenantData[t1] \cap tenantData[t2] = {}
\* Package consistency: installed packages must be in installed or disabled state
PackageConsistency ==
\A t \in Tenants, p \in installedPackages[t]:
packageStates[p] \in {"installed", "disabled", "installing"}
\* DBAL safety: no queries processed in error state
DBALSafety ==
dbalState = "error" =>
~\E u \in Users, r \in DataRecords:
WriteData(u, r) \/ DeleteData(u, r)
\* Audit completeness: all privileged operations are logged
AuditCompleteness ==
\A i \in 1..Len(auditLog):
auditLog[i].action \in {
"read_data", "write_data", "delete_data",
"modify_user_level", "install_package",
"uninstall_package", "toggle_package"
}
-----------------------------------------------------------------------------
(* Liveness Properties *)
\* Eventually, DBAL processes all queries (if it stays ready)
EventualProcessing ==
activeQueries /= {} ~> (activeQueries = {} \/ dbalState /= "ready")
\* If DBAL enters error state, it eventually recovers
EventualRecovery ==
dbalState = "error" ~> dbalState = "ready"
\* Package installation eventually completes
EventualPackageInstall ==
\A p \in Packages:
packageStates[p] = "installing" ~> packageStates[p] = "installed"
-----------------------------------------------------------------------------
(* System Specification *)
Spec ==
/\ Init
/\ [][Next]_vars
/\ WF_vars(DBALCompleteProcessing)
/\ WF_vars(DBALRecover)
/\ \A p \in Packages: WF_vars(CompletePackageInstall(p))
-----------------------------------------------------------------------------
(* Invariants to Check *)
Invariants ==
/\ TypeOK
/\ TenantIsolation
/\ PermissionEnforcement
/\ DataConsistency
/\ PackageConsistency
/\ DBALSafety
/\ AuditCompleteness
=============================================================================