hashirama/xserver
Watch
0
0
Fork
You've already forked xserver
 0
mirror of https://github.com/X11Libre/xserver.git synced 2026-10-21 01:13:38 +00:00
Code Issues Projects Releases Wiki Activity

Xext/namespace: fix memory leak during namespace destruction

Browse source 
When a transient namespace is deleted, XnsDestroyNamespace() frees the
namespace struct, its name, and its authentication tokens. However, it
leaves the virtual root window active in the server's resource database.

Because the virtual root window is never freed, the server leaks a Window
structure, window attributes, and properties every time a temporary
namespace is destroyed.

Fix this leak by calling FreeResource() on the virtual root window
before destroying the namespace.

Also update the formal TLA+ model in doc/Xnamespace.tla to track
resource cleanup and verify the fix.

Signed-off-by: Mason Green <mason@greenm01.net>
This commit is contained in:
Mason Green 2026-08-07 09:18:19 -04:00 • committed by Enrico Weigelt
commit 999015f6cd
2 changed files with 62 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

5
Xext/namespace/config.c
View file

@ -482,6 +482,11 @@ void XnsDestroyNamespace(struct Xnamespace *ns)
if (!ns || ns->builtin)
return;
if (ns->rootWindow) {
FreeResource(ns->rootWindow->drawable.id, RT_NONE);
ns->rootWindow = NULL;
}
/* detach any clients still pointing here so their later teardown does not
dereference freed memory (refcnt is being discarded with the namespace) */
for (int i = 1; i < currentMaxClients; i++) {

70
doc/Xnamespace.tla
View file

@ -14,6 +14,8 @@
* 3. Global Root Redirection: Global root window property operations are
* redirected to the client namespace's virtual root, preventing cross-namespace
* covert channel communications.
* 4. Virtual Root Lifetime (Memory Leak Prevention): Destroys virtual root windows
* on namespace deletion to prevent severe memory leaks in transient sessions.
*)
EXTENDS Naturals, Sequences, TLC
@ -24,11 +26,12 @@ CONSTANTS
ResourceTypes \* {"Window", "Pixmap", "Selection", "Property"}
VARIABLES
client_ns, \* Map of Client -> Namespace ("root" represents superPower)
resources, \* Set of active resource structures: [id: Nat, rtype: ResourceTypes, owner: Clients, ns_prefix: {"none"} \union Namespaces]
root_window, \* Resource ID of the real screen root window
ns_root_win, \* Map of Namespace -> Resource ID of virtual root windows
next_res_id \* Counter for resource ID generation
client_ns, \* Map of Client -> Namespace ("root" represents superPower)
active_namespaces, \* Set of currently active namespaces (dynamic)
resources, \* Set of active resource structures: [id: Nat, rtype: ResourceTypes, owner: Clients, ns_prefix: {"none"} \union Namespaces]
root_window, \* Resource ID of the real screen root window
ns_root_win, \* Map of Namespace -> Resource ID of virtual root windows
next_res_id \* Counter for resource ID generation
-----------------------------------------------------------------------------
@ -44,6 +47,7 @@ SameNamespace(c1, c2) == client_ns[c1] = client_ns[c2]
TypeOK ==
/\ client_ns \in [Clients -> Namespaces]
/\ active_namespaces \subseteq Namespaces
/\ root_window \in Nat
/\ ns_root_win \in [Namespaces -> Nat]
/\ next_res_id \in Nat
@ -55,6 +59,7 @@ TypeOK ==
Init ==
/\ client_ns \in [Clients -> Namespaces]
/\ active_namespaces = {"root", "NS_A"}
/\ root_window = 1
\* Virtual root windows created for each namespace
/\ ns_root_win = [ns \in Namespaces |-> IF ns = "root" THEN 1 ELSE 1 + (CHOOSE x \in 2..10 : TRUE)] \* Simplified mapping
@ -75,7 +80,7 @@ CreateResource(c, rtype) ==
IN
/\ resources' = resources \union {new_res}
/\ next_res_id' = next_res_id + 1
/\ UNCHANGED <<client_ns, root_window, ns_root_win>>
/\ UNCHANGED <<client_ns, active_namespaces, root_window, ns_root_win>>
\* 2. A client gets/sets a window property (XACE_PROPERTY_ACCESS)
\* - If a client accesses the real root window, Xnamespace redirects it to their virtual root window!
@ -97,7 +102,7 @@ GetSetProperty(c, target_win_id) ==
\/ \exists r_eff \in resources :
/\ r_eff.id = effective_win_id
/\ (SameNamespace(c, r_eff.owner) \/ effective_win_id = ns_root_win[client_ns[c]])
/\ UNCHANGED <<client_ns, resources, root_window, ns_root_win, next_res_id>>
/\ UNCHANGED <<client_ns, active_namespaces, resources, root_window, ns_root_win, next_res_id>>
\* 3. A client requests a selection (PRIMARY/CLIPBOARD)
\* - Selection isolation is enforced in hookSelectionFilter() by prepending client's namespace to the selection atom name.
@ -113,7 +118,7 @@ GetSetSelection(c, name) ==
(s.rtype = "Selection" /\ s.id = next_res_id - 1) => s.ns_prefix = client_ns[c]
/\ resources' = resources \union {new_sel}
/\ next_res_id' = next_res_id + 1
/\ UNCHANGED <<client_ns, root_window, ns_root_win>>
/\ UNCHANGED <<client_ns, active_namespaces, root_window, ns_root_win>>
\* 4. A client attempts to send an event (X_SendEvent) to another client's window
SendClientEvent(c, target_win_id) ==
@ -122,7 +127,35 @@ SendClientEvent(c, target_win_id) ==
/\ r.id = target_win_id
\* Allowed if same namespace or superPower (hookSend / clientAllowedOnClient)
/\ (SameNamespace(c, r.owner) \/ IsSuperPower(c))
/\ UNCHANGED <<client_ns, resources, root_window, ns_root_win, next_res_id>>
/\ UNCHANGED <<client_ns, active_namespaces, resources, root_window, ns_root_win, next_res_id>>
\* 5. Dynamic creation of a namespace (XnsCreate() / ProcXnsCreateNamespace())
CreateNamespace(c, ns) ==
/\ IsSuperPower(c)
/\ ns \notin active_namespaces
/\ active_namespaces' = active_namespaces \union {ns}
\* Create and register the namespace's virtual root window in resources database
/\ LET
v_root == [id |-> next_res_id, rtype |-> "Window", owner |-> c, ns_prefix |-> ns]
IN
/\ resources' = resources \union {v_root}
/\ ns_root_win' = [ns_root_win EXCEPT ![ns] = next_res_id]
/\ next_res_id' = next_res_id + 1
/\ UNCHANGED <<client_ns, root_window>>
\* 6. Dynamic teardown of a namespace (XnsDestroyNamespace() / XnsDelete())
\* - Buggy behavior (as-is): Removes the namespace but leaves the virtual root window in resources!
\* - Fixed behavior: Removes the namespace AND unregisters its virtual root window from resources.
DestroyNamespace(c, ns) ==
/\ IsSuperPower(c)
/\ ns \in active_namespaces
/\ ns /= "root" \* Builtin root namespace cannot be destroyed
/\ active_namespaces' = active_namespaces \ {ns}
\* MODELING BUGGY BEHAVIOR: Forget to clean up resources, keeping the rootWindow.
\* TO MODEL THE FIXED BEHAVIOR (our patch): Change `resources' = resources` to remove the virtual root window:
\* resources' = { r \in resources : r.id /= ns_root_win[ns] }
/\ resources' = resources
/\ UNCHANGED <<client_ns, root_window, ns_root_win, next_res_id>>
-----------------------------------------------------------------------------
@ -133,22 +166,24 @@ Next ==
\/ \exists c \in Clients, win_id \in Nat : GetSetProperty(c, win_id)
\/ \exists c \in Clients : GetSetSelection(c, "PRIMARY")
\/ \exists c \in Clients, win_id \in Nat : SendClientEvent(c, win_id)
\/ \exists c \in Clients, ns \in Namespaces : CreateNamespace(c, ns)
\/ \exists c \in Clients, ns \in Namespaces : DestroyNamespace(c, ns)
Spec == Init /\ [][Next]_<<client_ns, resources, root_window, ns_root_win, next_res_id>>
Spec == Init /\ [][Next]_<<client_ns, active_namespaces, resources, root_window, ns_root_win, next_res_id>>
-----------------------------------------------------------------------------
\* --- SECURITY INVARIANTS TO VERIFY ---
\* --- SECURITY & MEMORY INVARIANTS TO VERIFY ---
\* 1. Resource Confidentiality:
\* A non-root client can never successfully create, read, or modify a resource
\* owned by a client in a different non-root namespace.
Confidentiality ==
\forall r \in resources :
(r.ns_prefix /= "none" /\ r.ns_prefix /= "root") =>
(r.ns_prefix /= "none" /\ r.ns_prefix /= "root" /\ r.ns_prefix \in active_namespaces) =>
(r.ns_prefix = client_ns[r.owner] \/ IsSuperPower(r.owner))
\* 2. Clipboard Isolation (No Cross-Namespace Clipboard Sniffing):
\* 2. Clipboard Isolation:
\* No selection resource with a namespace prefix 'NS_A' can ever be owned
\* or accessed by a client belonging to a different namespace 'NS_B'.
ClipboardIsolation ==
@ -156,4 +191,13 @@ ClipboardIsolation ==
(s.rtype = "Selection" /\ s.ns_prefix /= "none") =>
(s.ns_prefix = client_ns[s.owner])
\* 3. No Resource Leakage (Memory Leak Proof):
\* If a namespace is destroyed, its corresponding virtual root window MUST
\* be cleaned up and removed from the active resources database.
\* (This Invariant fails under the buggy DestroyNamespace logic!)
NoResourceLeakage ==
\forall ns \in Namespaces :
(ns \notin active_namespaces) =>
\forall r \in resources : r.id /= ns_root_win[ns]
=============================================================================