From 4a85077f0201cd7c0741d6cafccd95568614f890 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 27 Dec 2025 01:54:25 +0000 Subject: [PATCH 1/2] Initial plan From cbb257d914d04508945cd206d7811a51b5298a45 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 27 Dec 2025 01:59:07 +0000 Subject: [PATCH 2/2] Add formal TLA+ specification for MetaBuilder MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Created spec/metabuilder.tla with comprehensive formal specification - Modeled 6-level permission system (Public → User → Moderator → Admin → God → Supergod) - Defined multi-tenant data isolation invariants - Specified DBAL state machine with security properties - Included package management operations - Added safety properties: TenantIsolation, PermissionEnforcement, DataConsistency - Added liveness properties: EventualProcessing, EventualRecovery - Created spec/metabuilder.cfg for TLC model checker configuration - Added spec/README.md with comprehensive documentation and usage guide Co-authored-by: johndoe6345789 <224850594+johndoe6345789@users.noreply.github.com> --- spec/README.md | 247 ++++++++++++++++++++++++++++ spec/metabuilder.cfg | 27 +++ spec/metabuilder.tla | 379 +++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 653 insertions(+) create mode 100644 spec/README.md create mode 100644 spec/metabuilder.cfg create mode 100644 spec/metabuilder.tla diff --git a/spec/README.md b/spec/README.md new file mode 100644 index 000000000..2a93bda63 --- /dev/null +++ b/spec/README.md @@ -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+ diff --git a/spec/metabuilder.cfg b/spec/metabuilder.cfg new file mode 100644 index 000000000..e675144a6 --- /dev/null +++ b/spec/metabuilder.cfg @@ -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 diff --git a/spec/metabuilder.tla b/spec/metabuilder.tla new file mode 100644 index 000000000..8d7726a5d --- /dev/null +++ b/spec/metabuilder.tla @@ -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 == <> + +----------------------------------------------------------------------------- +(* 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 {<>} + /\ auditLog' = Append(auditLog, [ + user |-> user, + action |-> "read_data", + tenant |-> userTenants[user], + level |-> userLevels[user] + ]) + /\ UNCHANGED <> + +\* 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 {<>} + /\ auditLog' = Append(auditLog, [ + user |-> user, + action |-> "write_data", + tenant |-> tenant, + level |-> userLevels[user] + ]) + /\ UNCHANGED <> + +\* 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 {<>} + /\ auditLog' = Append(auditLog, [ + user |-> user, + action |-> "delete_data", + tenant |-> tenant, + level |-> userLevels[user] + ]) + /\ UNCHANGED <> + +\* Query completes and is removed from active set +CompleteQuery(user, tenant, operation) == + /\ <> \in activeQueries + /\ activeQueries' = activeQueries \ {<>} + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* 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 <> + +----------------------------------------------------------------------------- +(* 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 <> + +\* Package installation completes +CompletePackageInstall(pkg) == + /\ packageStates[pkg] = "installing" + /\ packageStates' = [packageStates EXCEPT ![pkg] = "installed"] + /\ UNCHANGED <> + +\* 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 <> + +\* 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 <> + +----------------------------------------------------------------------------- +(* DBAL State Transitions *) + +\* DBAL starts processing a query +DBALStartProcessing == + /\ dbalState = "ready" + /\ activeQueries /= {} + /\ dbalState' = "processing" + /\ UNCHANGED <> + +\* DBAL completes processing and returns to ready +DBALCompleteProcessing == + /\ dbalState = "processing" + /\ dbalState' = "ready" + /\ UNCHANGED <> + +\* DBAL encounters an error (can recover) +DBALError == + /\ dbalState = "processing" + /\ dbalState' = "error" + /\ UNCHANGED <> + +\* DBAL recovers from error +DBALRecover == + /\ dbalState = "error" + /\ dbalState' = "ready" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* 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"}: + /\ <> \in activeQueries + +\* Permission enforcement: operations require appropriate level +PermissionEnforcement == + /\ \A u \in Users: + (\E t \in Tenants, op \in {"read", "write", "delete"}: + <> \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 + +=============================================================================