The total set is all possible configurations of the system denoted by \(\Omega\) or \(\mathcal{S}_{\text{total}}\).
The legal state is the state in which all the specified design constants of the system are realized; the set of all legal states denoted by \(\mathcal{L}\).
The illegal state is the state in which at least one of the design constants of the system is not realized; the set of illegal states is \(\Omega \setminus \mathcal{L}\).

A design invariant is a mandatory condition that must hold for every legal state \(s \in \mathcal{L}\).
If a state violates the invariant, it is illegal \(s \notin \mathcal{L}\).
where \(\mathcal{I}\) is the invariant (or conjunction of invariants).

It is the smallest indivisible execution step, with no observable intermediate state, moving the system from one state to another in a single step. Formally, we have a set of atomic actions . Each \(u_i\) is a function (or relation) from \(\Omega\) to \(\Omega\) (or a non-deterministic relation): \(u: \Omega \to \Omega\).
In an ownership system, an atomic action could be the allocation of a resource to an owner, the release of a resource, or the transfer of ownership. For \(\mathcal{R}=\{r\}\), \(\mathcal{O}=\{A\}\), initial state \(s_0: f(r)=0\), atomic action \(u_1\): allocate resource \(r\) to owner \(A\) gives \(s_0 \xrightarrow{u_1} s_1\) where \(s_1: f(r)=A\).
There are two types: deterministic (single outcome) and non-deterministic (multiple outcomes).

Action	System	Before state	After state
kmalloc(size)	Linux kernel	Free page (0)	Page owned by kernel
free(ptr)	Linux kernel	Page owned	Free page (0)
write(fd, buf, count)	System call	Data in buffer	Data written to file

Action	System	Before state	Possible after states	Reason
schedule()	Process scheduling	A process running	Any other ready process	CPU choice not fixed
interrupt_handler()	Interrupt handling	User instruction in progress	Return to same process or switch	Interrupt at any time
copy_from_user(to, from, size)	Linux kernel	Data in user space	Success or fault (page fault)	May fail if page paged out

The transition relation \(\mathcal{T}\) is the set of all pairs \((s,t)\) such that \(s\) is the state before executing an atomic action \(u\), \(t\) is the state after executing that atomic action \(u\), and there exists an atomic action \(u \in \mathcal{U}\) with \(u(s)=t\).
Formally, we can write:
In other words: And we can also write:

Reflexive Transitive Closure \(\mathcal{T}^*\)

\(\mathcal{T}^*\) is the set of all ordered pairs of states \((s,t)\) such that it is possible to go from \(s\) to \(t\) by following zero or more allowed transitions from the original relation \(\mathcal{T}\).
where : \(\mathcal{T}^0\) is the identity relation (no transition, i.e., \(s = t\)), and \( \mathcal{T}^0 = \{ (s, s) \mid s \in \Omega \} \) (zero steps) \( \mathcal{T}^1 = \mathcal{T} \) (one step) In other words, \(\mathcal{T}^*\) describes all reachability between states, including the reflexive (self‑pairs) and transitive (multi‑step) connections that are implicit in \(\mathcal{T}\).

Properties of \(\mathcal{T}^*\)

- \(\mathcal{T}^*\) is reflexive: \((s, s) \in \mathcal{T}^*\) for all \(s \in \Omega\).
- \(\mathcal{T}^*\) is transitive: if \((s, t) \in \mathcal{T}^*\) and \((t, u) \in \mathcal{T}^*\), then \((s, u) \in \mathcal{T}^*\).
- \(\mathcal{T}^*\) is the smallest relation containing \(\mathcal{T}\) that is both reflexive and transitive.
- Reachability description: \((s, t) \in \mathcal{T}^*\) if and only if there exists a path from \(s\) to \(t\) following the transitions in \(\mathcal{T}\).
- The set of states reachable from \(s_0\) is \(Reach(s_0) = \{ t \mid (s_0, t) \in \mathcal{T}^* \}\).
- Closure under composition: For any \(k, m \geq 0\), we have \(\mathcal{T}^k \circ \mathcal{T}^m = \mathcal{T}^{k+m}\)
- If \(\mathcal{T}\) is finite, then \(\mathcal{T}^*\) is also finite, but it can be larger than \(\mathcal{T}\) due to the inclusion of all possible paths.

Example for \(\mathcal{T}\) and \(\mathcal{T}^*\) with \(\Omega = \{s_0, s_1, s_2, s_3, s_4\}\)

Suppose we have the following transitions:
- \(s_0 \xrightarrow{u_1} s_1\)
- \(s_1 \xrightarrow{u_2} s_2\)
- \(s_2 \xrightarrow{u_3} s_3\)
- \(s_3 \xrightarrow{u_4} s_4\)
Then:
- \(\mathcal{T} = \{ (s_0, s_1), (s_1, s_2), (s_2, s_3), (s_3, s_4) \}\)
- \(\mathcal{T}^0 = \{ (s_0, s_0), (s_1, s_1), (s_2, s_2), (s_3, s_3), (s_4, s_4) \}\)
- \(\mathcal{T}^1 = \mathcal{T}\)
- \(\mathcal{T}^2 = \{ (s_0, s_2), (s_1, s_3), (s_2, s_4) \}\)
- \(\mathcal{T}^3 = \{ (s_0, s_3), (s_1, s_4) \}\)
- \(\mathcal{T}^4 = \{ (s_0, s_4) \}\) Reachability description (from each state):
- From \(s_0\): reachable states are \(\{s_0, s_1, s_2, s_3, s_4\}\)
- From \(s_1\): reachable states are \(\{s_1, s_2, s_3, s_4\}\)
- From \(s_2\): reachable states are \(\{s_2, s_3, s_4\}\)
- From \(s_3\): reachable states are \(\{s_3, s_4\}\)
- From \(s_4\): reachable states are \(\{s_4\}\)

The path is the actual sequence of states that the system goes through during its evolution.
It is the foundation for analyzing dynamic behavior and detecting violations of design hypotheses.
A path is a finite or infinite sequence of states \(\mathcal{P}=(s_0,s_1,s_2,\ldots)\) such that each consecutive pair is related by the transition relation \(\mathcal{T}\), i.e \((s_i, s_{i+1}) \in \mathcal{T} \quad \forall i\).
The length of a path \(\mathcal{P}\) is the number of transitions it contains, denoted \(|\mathcal{P}|\).
For a finite path \(\mathcal{P}=(s_0,s_1,\ldots,s_k)\), we have \(|\mathcal{P}|=k\).
We can write more precisely \(\mathcal{P}=( (s_0 \xrightarrow{u_1} s_1), (s_1 \xrightarrow{u_2} s_2), \ldots, (s_{k-1} \xrightarrow{u_k} s_k) )\) where each \(u_k\) is the atomic action that causes the transition from \(s_{k-1}\) to \(s_k\), \(\forall k\in \mathbb{N}^*\).

Components of a Path

- States \(s_i\): belong to the state set \(\Omega\) or \(\mathcal{S}_{\text{model}}\).
- Atomic actions \(u_i\): belong to the set \(\mathcal{U}\) (deterministic or non‑deterministic).
- Path length: number of actions (or transitions) = \(k\). A zero‑length path is a single initial state.

Relation to Atomic Actions and Transition Relation

- Each pair \((s_i, s_{i+1})\) satisfies \((s_i, s_{i+1}) \in \mathcal{T}\).
- For deterministic actions: \(s_{i+1} = u(s_i)\).
- For non-deterministic actions: \(s_{i+1} \in u(s_i)\).

Determinism vs. Non‑determinism – Impact on Paths

- Deterministic system: for each initial state \(s_0\), there is a unique path.
- Non‑deterministic system: from the same initial state \(s_0\), a tree of paths branches out (multiple possible outcomes for the same action or several actions possible).

In the adversarial model, we consider all possible paths. The existence of just one path that leads to an illegal state is enough to violate the design hypothesis \(\mathcal{H}\).

The critical path is the shortest path (minimum number of transitions) that starts from a legal state \(s_0 \in \mathcal{L}\) and ends (or passes through) an illegal state \(s_n \notin \mathcal{L}\).

Length of the critical path (\(\mathcal{d}_{\text{pcrit}}\))

Interpretation of \(\mathcal{d}_{\text{pcrit}}\)

The critical path represents the most vulnerable route from a legal state to an illegal state, indicating the minimum number of steps required to violate the design hypothesis.

Note

- \((s_i, s_{i+1}) \in \mathcal{T}\) means that the transition from state \(s_{i}\) to state \(s_{i+1}\) is allowed in one atomic step (whether deterministic or non‑deterministic).
- Any path with length \(\mathcal{d}_{\text{pcrit}}\) is called a critical path.

Example

Suppose we have a system with the following states and transitions:
- Legal states: \(\mathcal{L} = \{s_0, s_1\}\)
- Illegal states: \(\Omega \setminus \mathcal{L} = \{s_2, s_3\}\)
- Transition relation \(\mathcal{T}\): \((s_0, s_1) \in \mathcal{T}\), \((s_1, s_2) \in \mathcal{T}\), \((s_0, s_3) \in \mathcal{T}\)
In this example, there are two paths from legal states to illegal states:
1. \(s_0 \xrightarrow{u_1} s_1 \xrightarrow{u_2} s_2\) (length 2)
2. \(s_0 \xrightarrow{u_3} s_3\) (length 1)
The critical path is the second one, with length \(\mathcal{d}_{\text{pcrit}} = 1\), indicating that there is a direct transition from a legal state to an illegal state, which represents a severe vulnerability in the system.

The set of states that can be reached from an initial state \(s_0\) by applying any number (including zero) of allowed transitions \(\mathcal{T}\) is denoted \(Reach(s_0)\).

For every legal initial state \(s_0 \in \mathcal{L}\), all states reachable (via any number of allowed transitions) remain legal. That is, the system can never leave the legal region if it starts there.
< Meaning: It is the designer’s commitment that the design invariants are preserved throughout all possible executions. If \(\mathcal{H}\) holds, the system is safe with respect to the properties defining \(\mathcal{L}\). If false, there exists at least one path starting from \(\mathcal{L}\) and ending in \(\Omega \setminus \mathcal{L}\).

The Adversarial Model is a set of assumptions about the adversary’s capabilities and behavior, used to analyze the system’s security under worst‑case conditions. In Bytrep, the adversary controls every non‑deterministic or unpredictable aspect of execution.
Core assumptions: maximal concurrency, hostile scheduling, adversarial interleaving, no environmental goodwill, no reliance on typical execution paths.
Mathematical formulation: where \(Reach_{adv}(s_0)\) includes all paths the adversary can enforce (by any ordering, and by choosing any non‑deterministic transitions).
Role in Bytrep methodologies: ensures identified vulnerabilities are valid even in worst‑case scenarios.

The failure domain defines the scope of corruption when a design invariant is violated. It determines which parts of the system become compromised and which remain intact.
Definition: Let \(\mathcal{F} \subseteq \Omega\) be the set of states that can become corrupted after a violation of an invariant \(I\) (i.e., after reaching an illegal state). \(\mathcal{F}\) is the smallest set closed under \(\mathcal{T}\) that contains the first illegal state.
Properties: containment (resilient if \(\mathcal{F} \subsetneq \Omega\)), size (smaller \(\mathcal{F}\) better), stability (closed under \(\mathcal{T}\)), propagation (larger \(\mathcal{F}\) wider impact), isolation (well‑isolated if violations contained in small subset).

The Threat Model is an explicit and precise definition of the limits of the adversary’s capabilities and the assumptions about the environment in which the system operates. It differs from the Adversarial Model (which assumes worst‑case behavior within those limits) in that it sets the boundary rules that the adversary cannot exceed.
Mathematical definition: A threat model \(\Theta\) is defined by three main components: (1) Set of atomic actions the adversary can influence \(U_{threat}\); (2) Set of observations the adversary can make \(O_{adv}\); (3) Variables or components that remain outside the adversary’s control \(C_{\text{secure}}\). Thus, any security claim is only valid with respect to \(\Theta\).
Threat Model gives the rules; Adversarial Model tests worst‑case behavior; Failure Domain analyzes consequences after a violation.

Design legitimacy is the justification for a design to exist within a hostile, long-lived system. Correctness does not imply legitimacy. A design may be structurally correct and still impose unjustified adversarial cost.
Key criteria: length of the critical path (shorter → lower adversarial cost, design may become illegitimate), size of the failure domain \(\mathcal{F}\) (larger → greater damage, reducing legitimacy), benefit vs. cost.
Example (lock without starvation protection): the design is correct (mutual exclusion preserved), yet a single adversary can hold the lock forever at very low cost → illegitimate.

Projection from Total Space \(\Omega\) Define a projection : that selects relevant dimensions (e.g., owner, life state) and ignores others. \(\mathcal{S}_{\text{model}}\) is the raw abstract space, image of the projection: By convention, \(\mathcal{S}_{\text{model}}\) is identified with a subset of \(\Omega\) by fixing default values for ignored dimensions. Legal states of the model: with Invariants \(\mathcal{I} = \{i_1,i_2,\dots\}\) are absolute: independent of time and context, evaluated only on abstract states.

is a deterministic transition function, and the Axioms are:
(1) Structural Isolation: algebraic identity invariant under projection,
(2) Absoluteness of Local Invariants: each invariant evaluated strictly inside \(\mathcal{S}_{\text{legal}}\),
(3) Chronological Staticism: \(\partial i / \partial t = 0 ,\forall i \in \mathcal{I}\).
\(\delta\) is a deterministic rule: if the system is in legal state \(s\), \(\delta(s)\) gives the unique next state \(t\). No choice, no randomness, no adversary. Condition: allowed by invariants and independent of external factors (thread identity, scheduling, timing, adversary, hardware).
Examples of correct \(\delta\): simple counter model \(\{0,1,2\}\) with invariant "counter only increases" → \(\delta(0)=1,\delta(1)=2,\delta(2)=2\). Invalid example: counter that allows both increment and decrement from state 1 – non‑deterministic, requires ELTS.
\(\mathcal{M}\) is a deterministic, idealized model that captures the core design invariants but abstracts away all adversarial and temporal complexities. It serves as the baseline for correctness analysis, while ELTS is needed to analyze security properties. ELTS extends \(\mathcal{M}\) with non‑determinism, adversary \(\mathcal{A}\), threat \(\Theta\), failure \(\mathcal{F}\), time, scheduling, and execution environment. ELTS reveals vulnerabilities invisible in \(\mathcal{M}\).
Historical note: LTS introduced by Robert M. Keller (1976); ELTS adds adversarial and temporal dimensions.
Comparison table:

Feature	\(\mathcal{M}\) (Core)	ELTS (Enriched)
Transitions	Deterministic	Non‑deterministic (adversary choice)
Time	Timeless	Scheduling, interleavings, clocks
Adversary	Absent	Present (\(\mathcal{A}\))
Concurrency	Absent	Races, threads
Goal	Formal verification	Exploitable vulnerability discovery