Filament: Denning-Style Information Flow Control for Rust
arXiv:2604.14357v1 [cs.PL] 15 Apr 2026
JEFFREY C. CHING, Duke University, USA QUAN ZHOU, Google, USA DANFENG ZHANG, Duke University, USA Existing language-based information-flow control (IFC) tools face a fundamental tension: Denning-style systems that track explicit and implicit flows at the variable level typically require compiler modifications, while more coarse-grained approaches, including recent work Cocoon, avoid compiler changes but impose more restrictive programming models. We present Filament, a Denning-style static IFC library for Rust that requires no compiler modifications. Filament addresses three key challenges in building a practical IFC library for Rust. First, it enables fine-grained explicit-flow checking with minimal annotation overhead by leveraging Rust’s type inference. Second, it introduces pc_block!, a lightweight construct for enforcing implicit flows via a compile-time program counter label, without requiring compiler support. Third, it provides fcall! and mcall! macros to support seamless and safe interoperability with standard and third-party libraries. Our evaluation shows that Filament incurs negligible compile-time overhead and requires only modest annotations. Moreover, compared to Cocoon, Filament offers a more permissive programming model, reducing the need for frequent escape hatches that bypass security checks. CCS Concepts: • Security and privacy → Security requirements; Software security engineering. Additional Key Words and Phrases: Information Flow Control; Type Systems; Rust
1
Introduction
Information flow control (IFC) is a fundamental mechanism for ensuring that sensitive data is accessed and transmitted only in accordance with established security policies. By regulating how information propagates through a system, it helps prevent unauthorized disclosure and supports the preservation of confidentiality, integrity, and privacy. Denning’s seminal work [10], which we term as Denning-style IFC, introduced a precise, fine-grained framework that tracks information flow through both explicit assignments and implicit control dependencies using a lattice model of security classes [9]. It is characterized by: • A program counter (𝑝𝑐) label, which tracks the security level of the current control-flow context, in order to control implicit flows introduced by branches and loops. • IFC checks at each instruction to control both explicit and implicit flows. Compared with coarse-grained IFC systems such as those based on the Bell–LaPadula model [5], which enforce a simple lattice-based policy known as “no read up, no write down,” at the granularity of entire subjects and objects (e.g., processes and files), Denning-style IFC offers increased precision (fewer unnecessary rejections of safe programs) via reasoning about information propagation within complex software systems, as well as provable end-to-end guarantees about confidentiality and integrity [27, 34, 39]. This strong theoretical basis has enabled practical language implementations such as Jif [3, 24, 25] and its variants [7, 23]. However, due to the inherent complexity of Denning-style IFC, existing implementations typically require modifications to both the programming language and its compiler, including customized type-checking and inference rules. These requirements significantly hinder the practical adoption of these well-founded techniques. In particular, it is both costly and time-consuming to rewrite large existing software systems in specialized languages and to maintain customized compilers to keep pace with their underlying base language features. Authors’ Contact Information: Jeffrey C. Ching, Duke University, Durham, NC, USA, [email protected]; Quan Zhou, Google, USA, [email protected]; Danfeng Zhang, Duke University, Durham, NC, USA, [email protected].
2
Jeffrey C. Ching, Quan Zhou, and Danfeng Zhang
These limitations have motivated a promising line of recent work [4, 13, 20, 32, 33] that investigates how IFC can be enforced through lightweight libraries layered on top of mainstream programming languages. For example, Russo et al. [33] propose a monadic library for Haskell in which confidential values are encapsulated within an abstract security type, Sec. By construction, the only way to manipulate secret values is through the monadic operations provided by the library. Because such effective systems are generally not supported by mainstream imperative languages such as Java, C, and Rust, a recent work Cocoon [20] introduces the first static IFC mechanism for the Rust language. Notably, Cocoon ensures that all reads and writes involving secret values occur within lexically-scoped regions, called secret blocks, which are introduced via the secret_block macro. For example, the Cocoon code snippet below performs a computation over x and y and stores the result in z, where x and z are secret while y is public: 1 2 3 4 5 6 7 8
#[side_effect_free_attr] fn foo(x: i32, y: i32) → i32 { x + y } let x = secret_block!(lat::A { wrap_secret(1) }); let y = 2; let z: Secret<i32, lat::A> = secret_block!( lat::A { let u_x = unwrap_secret(x); wrap_secret(foo(u_x, y)) });
In Cocoon, non-public values are wrapped in the abstract type Secret, e.g., Secret⟨i32, lat :: A⟩ denotes an integer classified at level A. Accessing or modifying such values requires execution within a secret block (e.g., lines 4 and 7–8), the only lexically scoped region in which non-public values may be revealed using the macro unwrap_secret (e.g., line 7). Cocoon enforces several restrictions to preserve security guarantees. For a secret block with level L, the block may (1) unwrap values whose security level is no higher than L (e.g., line 7); (2) modify non-local variables whose security level is no lower than L; (3) return values classified exactly at level L (e.g., line 8); and (4) invoke only side-effect-free functions, i.e., functions that do not write to variables visible outside their local scope (e.g., function foo, annotated at line 1). Since all of those restrictions are applied to the entire secret block, we term such an enforcement block-level IFC, to contrast with the Denning-style IFC that tracks 𝑝𝑐 labels and checks information flows for each individual expression and command. In this paper, we present Filament, the first Denning-style IFC system for a mainstream imperative language without changing the compiler. Similar to Cocoon and its successor Carapace [4], Filament is implemented as a Rust library for unmodified Rust and operates with the standard Rust compiler. However, Filament advances beyond Cocoon’s block-level protection by weaving fine-grained IFC directly at the level of individual instructions via the following novel features: • Rather than unwrapping (i.e., downgrading) non-public values within secret blocks, Filament employs a relabel! macro to explicitly upgrade sensitivity when necessary. Consequently, secret values are not required to remain confined within designated secret blocks1 . • In contrast to conservatively prohibiting all side effects within a secret block, Filament introduces a pc_block! construct to track the 𝑝𝑐 label. Under this mechanism, only side effects whose sensitivity is lower than the current 𝑝𝑐 are disallowed. As a result, Filament eliminates the need for the no-side-effect requirement check for majority of functions. • To make it compatible with the Rust standard library and third-party crates, Filament leverages Rust’s type system and introduces novel macros, such as fcall! and mcall!. These 1 By eliminating the secret blocks used in Cocoon, whose implementation relies on auto traits and negative traits not
available in stable Rust, Filament remains compatible with stable Rust, which is an additional benefit of its novel design.
Filament : Denning-Style Information Flow Control for Rust
3
macros enable labeled values to be passed through unlabeled function calls without requiring declassification, while soundly tracking label propagation across library boundaries. • Filament takes advantage of the Rust trait system and type inference system to reduce the annotation burden on programmers. As a result, Filament avoids frequent use of annotations such as unwrap_secret and wrap_secret in Cocoon programs. Together, the metaprogramming layer introduced by Filament effectively bridges the gap between Denning-type IFC and Rust’s existing type system, allowing IFC on top of a stable Rust compiler. For example, the following Filament code is equivalent to Cocoon code above: 1 2 3 4
fn foo(x: i32, y: i32) → i32 { x + y } let x = Labeled::<i32, A>::new(1); let y = 2; let z = fcall!(foo(x, relabel!(y, A)));
We note that Filament provides the following benefits due to its novel features described above: • Filament eliminates the need for secret blocks, side-effect checks, and explicit wrapping and unwrapping operations present in the Cocoon equivalent. As a result, Filament code more closely resembles the original Rust code written without IFC mechanisms. • When invoking the function foo with a non-public parameter x, the macro fcall! automatically lifts the parameter and returns types of foo to the secret type Labeled::<i32, A>. Additionally, the macro relabel! is used to upgrade y to the same security level. • Leveraging Rust’s type inference system, Filament requires only minimal type annotations. We implement Filament as a Rust library built on Rust 1.69 and have open-sourced it at [1]. To evaluate its practicality, we re-implemented all four applications from the Cocoon code repository [2], along with an additional application, JPMail [15], originally developed in Jif. Our evaluation yields several important findings. First, Filament enforces security guarantees comparable to prior approaches while requiring only minimal to moderate code modifications across all applications. Second, although Filament adopts a fine-grained, Denning-style IFC model, the annotation burden remains low in practice due to its design, which leverages Rust’s type inference mechanisms. Third, Filament provides a more permissive programming model than Cocoon: it eliminates 12 unnecessary declassification and unchecked operations present in Cocoon’s implementations, thereby reducing potential risks for unintended information leakage. Finally, we observe that the compile-time overhead with Filament is low and scales well to large codebases. In summary, this paper makes the following contributions: • We develop the first Denning-style information flow tool in Rust without requiring compiler modifications. • We design Filament to address key challenges in Denning-style IFC for Rust by enabling fine grained information flow tracking with low annotation burden, supporting implicit flow tracking via pc_block! without compiler changes, and ensuring seamless and safe interoperability with external libraries through fcall! and mcall!. • Compared to Cocoon, Filament requires less code modification and is more faithful to the original program. Moreover, the permissive programming model of Filament also removes unnecessary declassification in Cocoon code. • We present a performance evaluation demonstrating that Filament’s low compile-time overhead and minimal annotation burden.
4
Jeffrey C. Ching, Quan Zhou, and Danfeng Zhang
2
Background and Overview
2.1
Secrecy Labels and Lattice
As is standard in IFC systems, we associate all data with security labels dawn from a predefined security lattice L. Two labels ℓ1 and ℓ2 from the lattice are ordered, written ℓ1 ⊑ ℓ2 , if information at ℓ2 is at least as restrictive as information at ℓ1 (in other words, data labeled with ℓ1 can safely flow to ℓ2 ). In a confidentiality lattice, ℓ1 ⊑ ℓ2 means that ℓ2 is more sensitive than ℓ1 , while in an integrity lattice, ℓ1 ⊑ ℓ2 means that ℓ1 is more trusted than ℓ2 . Without loss of generality, we assume a “diamond” lattice with four labels: ⊥ (public), ℓ𝐴 , ℓ𝐵 , and ℓ𝐴𝐵 , ordered as ⊥ ⊑ ℓ𝐴 ⊑ ℓ𝐴𝐵 and ⊥ ⊑ ℓ𝐵 ⊑ ℓ𝐴𝐵 throughout the paper. The join operation ℓ1 ⊔ ℓ2 returns the least upper bound of two labels in the lattice, representing the most permissive label that is at least as restrictive as both ℓ1 and ℓ2 . For example, ℓ𝐴 ⊔ ℓ𝐴𝐵 = ℓ𝐴𝐵 and ℓ𝐴 ⊔ ℓ𝐵 = ℓ𝐴𝐵 . 2.2
Denning-Style IFC
Early IFC systems, such as those based on the Bell–LaPadula model [5], enforced simple latticebased policies commonly summarized as “no read up, no write down.” These policies regulate information flow at the granularity of entire subjects and objects (e.g., processes and files). For instance, a process with label ℓ𝐴 cannot read data labeled ℓ𝐴𝐵 , nor can it write to data labeled public. Such enforcement mechanisms were primarily deployed in OS-level IFC systems [11, 40], as well as in dynamic IFC systems that raise security labels at runtime when sensitive data is accessed. However, under this model, once confidential data enters the execution context, the entire computation becomes effectively “tainted.” As a result, all subsequent outputs must be treated at the elevated security level associated with that data. This limitation leads to the well-known label creep problem [36, 38], in which the security level of a long-running process monotonically increases over time. Eventually, the process becomes so highly tainted that it can no longer produce outputs that are observable at lower security levels, such as public outputs. The seminal work of Denning [10] laid the foundation for modern fine-grained, languagebased IFC systems [34]. A key contribution of Denning’s model is the introduction of a program counter label (𝑝𝑐), which captures the sensitivity of the current control-flow context. The 𝑝𝑐 label is raised when program execution enters a branch whose condition depends on sensitive data. This mechanism enables IFC systems to precisely track implicit flows through control dependencies while avoiding the label creep problem: once execution exits the scope of the sensitive branch, the 𝑝𝑐 label can be restored to its previous label, thereby allowing subsequent computations to proceed without unnecessarily propagating high-security labels. For example, consider the following code: 1 2 3 4 5 6 7 8 9
let dataA: i32 = 10; // with label A, non-public let mut public: i32 = 0; public = dataA; // insecure explicit flow if dataA > 0 { // pc is set to label A public = 1; // insecure implcit flow } else { public = 2; // insecure implicit flow } // pc is set to public public = 2; // secure explicit flow
In this example, the variable dataA carries a non-public security label ℓ𝐴 , while public represents a public variable. The assignment at line 3 constitutes an explicit flow, as information from a nonpublic source is directly written into a public variable. The branch at line 4 illustrates an implicit flow. Since the branch condition depends on the non-public variable dataA, by observing if public is set to 1 or 2 after the branch, an attacker can reveal if dataA is greater than zero or not.
Filament : Denning-Style Information Flow Control for Rust
5
To eliminate both explicit and implicit insecure information flows, a Denning-style IFC system associates each program point with a program counter label (𝑝𝑐) that represents the sensitivity of the current control context. For every assignment statement of the form 𝑥 := 𝑒, the system enforces two constraints. First, to prevent explicit flows, the security label of the expression 𝑒 must be bounded by the label of the target variable 𝑥 (e.g., ℓ𝐴 ⊑ ⊥ at line 2, which does not hold). Second, to prevent implicit flows, the program counter label 𝑝𝑐 must also be bounded by the label of 𝑥 (e.g., ℓ𝐴 ⊑ ⊥ at lines 5 and 6, which does not hold). Note that 𝑝𝑐 is reset to public at line 9, after the sensitive branch. Consequently, the assignment at line 10 yields the constraints ⊥ ⊑ ⊥ for both explicit and implicit flow checks. These constraints trivially hold, and a Denning-style system therefore correctly concludes that the statement at line 10 is secure. Denning-style IFC can be formalized as a type system that provides provable end-to-end guarantees for both confidentiality and integrity [27, 34, 39]. This strong theoretical foundation has enabled the development of practical language-based implementations, including Jif [3, 24, 25] and several of its extensions and variants [7, 23]. 2.3
Cocoon and Block-Level IFC
Cocoon [20] represents an important step toward integrating static IFC into mainstream imperative programming languages. In Cocoon, programmers encapsulate sensitive data within a secret_block!, within which the system enforces the classical information-flow policy of “no read up, no write down.” By design, Cocoon is more permissive than coarse-grained IFC systems in two key respects: • Cocoon enforces IFC within the scope of individual secret blocks, rather than across an entire process or function. • Cocoon mitigates the label creep problem by restricting all uses of non-public values to secret blocks and by either verifying or assuming that functions invoked within these blocks are side-effect free. Consequently, the execution environment remains public outside the boundaries of the secret blocks. However, unlike Denning-style IFC systems, Cocoon does not maintain a 𝑝𝑐 label, nor does it enforce explicit and implicit flows by checking IFC constraints on the security labels of expressions. Instead, Cocoon unwraps non-public data within each secret block, verifies that the functions invoked inside the block are side-effect free, and taints the resulting outputs with the secrecy label associated with the enclosing secret block. Accordingly, we characterize Cocoon’s approach as enforcing block-level IFC in this paper. 2.4 Rust Rust is a modern programming language designed to provide strong safety guarantees without sacrificing performance. Its expressive type system, featuring traits, generics, lifetimes, and ownership semantics, enables the compiler to enforce rich correctness properties at compile time while still supporting low-level control over memory and concurrency. In the following, we introduce several Rust features on which Filament builds on. Traits. Rust’s trait system provides a mechanism for defining shared behavior abstractly, allowing types to implement specified interfaces and enabling polymorphism and code reuse through trait bounds and generic programming. For example, the standard library defines the Display trait for types that can be formatted as user-facing strings: 1 2 3
use std::fmt::Display; fn print_value<T: Display>(x: T) { println!("{}", x); }
6
Jeffrey C. Ching, Quan Zhou, and Danfeng Zhang
Here, the generic function print_value can accept any type that implements the Display trait, such as i32 or &str. Filament leverages Rust’s trait system to support user-defined security lattices (Section 2.1), enable static checking of flows-to relations over security labels, and compute the least upper bound (i.e., join operation) of these labels (Section 4.1). Generics and Phantom Types. Rust’s generics allow types and functions to be parameterized over arbitrary types subject to trait bounds. For example, 1 2 3
use std::fmt::Display; fn print_pair<T: Display>(x: T, y: T) { println!("({}, {})", x, y); }
Here, the function print_pair is generic over the type parameter T, while the trait bound T: Display requires that any instantiation of T implement the Display trait. Filament uses Rust generics to wrap values of any data type to an abstract security labeled values (Section 4.1) and also utilize generics to lift label-less functions to handle labeled values (Section 4.4). Moreover, Rust supports phantom types through the PhantomData marker type, which allows programmers to associate a generic type parameter with a data structure without storing a value of that type. This pattern is commonly used to encode additional compile-time information without affecting the runtime representation. To enforce Denning-style IFC without incurring runtime penalties, we leverage Rust’s phantom type to associate security labels with their corresponding data into the type system (Section 4.1). 3
Motivating Examples
As discussed in Section 2, Cocoon enforces block-level IFC, whereas Filament adopts Denning-style IFC. In theory, fine-grained and coarse-grained IFC have been shown to be equally expressive in both static [28, 30] and dynamic [38] settings. Nevertheless, we draw on several concrete code examples from Cocoon’s repository [2] to illustrate that Denning-style IFC provides a more appealing programming model for developers. Specifically, although it is theoretically possible to rewrite Cocoon programs to overcome the limitations discussed below, our examples suggest that developing IFC-enabled programs in Filament is more intuitive and natural for programmers. Moreover, the resulting code remains closer to standard Rust code written without IFC, making it easier to port existing Rust projects to Filament. 3.1
Annotation Burden and Unchecked Functions
Figure 1a presents a code snippet from Cocoon’s implementation of the Battleship game, a classic two-player board game in which each player places ships at secret locations on a grid, and the placement of each player’s ships must remain confidential from the opponent. Due to its conceptual simplicity coupled with non-trivial security requirements, Battleship has been widely used as a case study in prior IFC systems [3, 17]. To protect the confidentiality of ship_positions, the initialization logic must be enclosed within a secret_block! (lines 3–9). Furthermore, every function invoked within this block, including random_placement (line 14) and place_ship (line 17), must be individually annotated with #[side_effect_free_attr]. This manual annotation requirement increases with the depth of the call chain, since any function invoked by an annotated function must also be free of side effects. Beyond the annotation burden, a more significant limitation is that disallowing all side effects can be overly restrictive. For instance, at line 20, the function place_ship must update external data stored in grid, which inherently introduces side effects. Cocoon’s current workaround is to wrap
Filament : Denning-Style Information Flow Control for Rust 1 2 3 4 5 6 7 8 9 10 11
7
impl<L: lat::Label> Player<L> { fn new() → Player<L> { let ship_positions = secret_block!(L { let ships = [...]; let mut ship_positions: Grid<bool> = [[false; GRID_SIZE]; GRID_SIZE]; for ship in ships { let placement = random_placement(&ship_positions, &ship); place_ship(&mut ship_positions, &placement); }wrap_secret(ship_positions) }); ... }}
12 13 14
#[side_effect_free_attr] fn random_placement(grid: &Grid<bool>, ship: &Ship) → Placement
15 16 17 18 19 20 21 22
#[side_effect_free_attr] fn place_ship(grid: &mut Grid<bool>, placement: &Placement) { ... while row<placement.start_row+placement.size && col<placement.start_col+placement.size { unchecked_operation(grid[row][col] = true); ... }}
(a) Implementation of Battleship guess in Cocoon. 1 2 3 4 5 6 7 8 9 10
impl<L: Label> Player<L> { pub fn new() → Player<L> { let ships: [Ship; 5] = [ ... ]; let mut ship_positions = Labeled::<Grid<bool>, L>::new([[false; GRID_SIZE]; GRID_SIZE]); for ship in &ships { let placement = random_placement(&ship_positions, ship); place_ship(&mut ship_positions, &placement); } ... }}
11 12 13 14 15 16
fn place_ship<L: Label>(grid: &mut Labeled<Grid<bool>, L>, placement: &Placement) { ... grid[row][col] = Labeled::<bool, L>::new(true); ... }}
(b) Implementation of Battleship guess in Filament. Fig. 1. The implementation of player function of battleship game in Filament and Cocoon.
such operations in unchecked_operation. However, this mechanism effectively bypasses IFC and may compromise its end-to-end soundness guarantees in such cases. To address these limitations, Filament tracks information flow at the level of individual variables, as shown in Figure 1b. Only the secret variable ship_positions is annotated with Labeled<Grid<bool >, L>, while no additional annotations are required due to Rust’s type inference system. Moreover, within the function place_ship, Filament can precisely determine that updates to grid are secure, since the corresponding parameter ship_positions carries a secret label. Hence, the Filament version is also more secure, as no IFC bypassing operations like unchecked_operation are required.
8
Jeffrey C. Ching, Quan Zhou, and Danfeng Zhang 1 2 3 4 5 6 7 8 9
let alice_cal: HashMap<String, Secret<lat::A,bool>> = // { "Monday" → Secret(true), ... } let bob_cal: HashMap<String, Secret<lat::B,bool>> = // { "Monday" → Secret(false), ...} let mut count = secret_block!(lat::AB { wrap_secret(0) }); for (day, available) in alice_cal { secret_block!(lat::AB { if unwrap_secret(available) && *unwrap_secret_mut_ref(...Option::unwrap(...HashMap::get(&bob_cal, &day))) { *unwrap_secret_mut_ref(&mut count) += 1; }});}
(a) Implementation of Calendar in Cocoon. 1 2 3 4 5 6 7 8 9
let alice_cal: HashMap<String, Labeled<lA,bool>> = // { "Monday" → Secret(true), ... } let bob_cal: HashMap<String, Labeled<B,bool>> = // { "Monday" → Secret(false), ...} let mut count = Labeled::<i32, AB>::new(0); for (day, available) in alice_cal { if let Some(bob_avail) = bob_cal.get(day) { pc_block!{(AB) { if *available && *bob_avail { count = count + 1; }}}};}
(b) Implementation of Calendar in Filament. Fig. 2. Implicit flow in the calendar example.
3.2
Implicit Flows
Figure 2a presents a code snippet from Cocoon’s implementation of a calendar program that determines the mutual availability of Alice and Bob, where each person’s calendar is considered confidential. Because Cocoon does not distinguish implicit flows from explicit flows, the entire branch between lines 6 and 9 must be enclosed within secret_block!, as the branch condition depends on Alice’s availability. As discussed in Section 3.1, code within the secret block requires frequent use of the unwrap annotation to perform computations on non-public values. In addition, all function calls within the block, including Option :: unwrap and HashMap :: get, must either be verified to side-effects free or be wrapped with unchecked_operation to bypass IFC enforcement. In contrast, Filament introduces a novel macro, pc_block!, to track 𝑝𝑐 labels at compile time, as illustrated in Figure 2b. At line 5, the 𝑝𝑐 label is annotated as lat::AB because the control flow depends on both Alice’s availability (line 4) and Bob’s availability (line 5). Within a pc_block! environment, Filament statically verifies that all modified variables have labels that are at least as restrictive as lat::AB, thereby preventing illegal implicit flows. For example, if the label of count were changed to lat::A, the assignment to count at line 8 would be rejected by the type system. We provide further details on this mechanism in Section 4.3. 3.3
Library Function Calls
Figure 3a presents a code snippet from Cocoon’s implementation of Spotify TUI, a terminal based Spotify client written in Rust. This application processes user credentials, including user IDs and passwords. So any information derived from or related to the password is treated as confidential. The application relies extensively on third party libraries. However, functions provided by these libraries, such as serde_yaml::from_str, are security-agnostic, meaning they expect plain Rust types rather than security labeled types. To accommodate this limitation, Cocoon requires programmers to (1) explicitly declassify inputs at each function call (lines 1, 9, and 10) in order to invoke these
Filament : Denning-Style Information Flow Control for Rust 1 2 3
9
let serde_yaml_str = serde_yaml::from_str(config_string.declassify_ref())?; let mut config_plain = secret_block!(lat::Label_A { wrap_secret(serde_yaml_str) }); self.device_id = Some(device_id.clone());
4 5 6 7 8 9 10
secret_block_no_return!(lat::Label_A { let u = unwrap_secret_mut_ref(&mut config_plain); u.device_id = Some(device_id); }); let new_config = serde_yaml::to_string(config_plain.declassify_ref())?; write!(config_file, "{}", new_config.declassify_ref())?;
(a) Implementation of Spotify TUI in Cocoon. 1 2 3 4 5
let mut config_plain = fcall!(serde_yaml::from_str::<ClientConfigSerde>(&config_string)?); self.device_id = Some(device_id.clone()); config_plain = mcall!(config_plain.with_device_id(device_id)); let new_config = fcall!(serde_yaml::to_string(&config_plain)?); mcall!(config_file.write(&new_config)?);
(b) Implementation of Spotify TUI in Filament. Fig. 3. Comparison of set_device_id function. Cocoon requires declassify_ref() at every serde and I/O call boundary, and a secret_block_no_return! with unwrap_secret_mut_ref to mutate a single field. Our library uses fcall! and mcall! to thread the label through all calls.
third party functions, and then (2) rewrap the returned values immediately afterward (line 2). However, this approach introduces a security risk, as it relies on programmers to manually restore the security labels after each call. If the programmer forgets to rewrap a returned value, the type system cannot detect the resulting vulnerability. For example, if the re-wrapping at line 2 is omitted and the code instead is let mut serializable_config = serde_yaml_str; Cocoon fails to detect the error, and the variable serializable_config may subsequently be leaked to the public! To overcome this limitation, Filament provides two macros, fcall! and mcall!, which automatically lift security-agnostic functions and methods to their labeled variants. As a result, the outputs of these functions and methods are automatically wrapped with the appropriate security label, avoiding the security flaw present in Cocoon’s approach. For example, in Filament ’s implementation shown in Figure 3b, config_string can be processed as a value of type Labeled<String, A> through fcall! without any manual declassification, and the returned value is lifted to the same security label. Further details of this mechanism are provided in Section 4.4. 4
Filament Design
This section presents Filament, a Denning-style static IFC system built on top of Rust. We begin by describing the program model underlying Filament in Section 4.1. Section 4.2 explains how Filament handles explicit information flows, while Section 4.4 discusses its treatment of function calls. Finally, Section 4.3 describes how Filament handles implicit flows. The new language constructs are summarized in Figure 4. 4.1
The Programming Model
Security Labels and Lattice. In Filament, user specifies a pre-defined lattice in two aspects. First, security labels are defined as distinguished types. Moreover, the ordering on security labels is governed by the FlowsTo trait, which is implemented for a label ℓ1 if and only if ℓ1 ⊑ ℓ2 in the security lattice. For example, the Rust implementation in Figure 5 defines the “diamond” security lattice
10
Jeffrey C. Ching, Quan Zhou, and Danfeng Zhang
Construct
Syntax
Definition
Creating & transforming labeled values Wrap
Labeled::<T,L>::new(v)
Create Labeled<T,L>
Relabel
relabel!(x, Target)
Upgrade label; compile error if 𝐿𝑥 @ Target
Declassify
declassify(x)
Downgrade to Public (escape hatch)
Function Calls & Method calls Function call
fcall!(f(a,&b))
Unwraps args, calls f, wraps result in most restrictive label among all argument labels
Method call
mcall!(obj.m(a))
Preserves receiver label 𝐿 on return value
Field access
mcall!(obj.field)
Field access preserving label 𝐿
pc_block!{(L){...}}
Initializes PC = 𝐿; rewrites all assignments to secure_assign_with_pc which checks both explicit and implicit flows; update PC at nested branches
Attribute (fn)
#[side_effect_free_attr]
Required attribute for functions in pc_block!
Unchecked
unchecked_operation(e)
Bypasses side-effect checks (escape hatch)
Implicit flow control PC block
Side-effect control
Fig. 4. Filament APIs.
shown to the left. Note that since Filament treats all “unlabeled” types as public data (i.e., label Public in a lattice), we only need to define three non-public labels and their relation in Figure 5c. Moreover, the join operation is defined as a trait that computes the least upper bound of two security labels at compile time, producing an associated output type Out that represents the resulting security level. For identical labels, the join is idempotent (e.g., 𝐴 ⊔ 𝐴 = 𝐴), whereas for distinct labels, the result corresponds to their least upper bound (e.g., 𝐴 ⊔ 𝐵 = 𝐴𝐵). A partial implementation is shown below. 1 2 3 4
pub trait Join<Other: Label>: Label {type Out: Label;} impl Join<A> for A {type Out = A;} impl Join<B> for A {type Out = AB;} impl Join<AB> for A {type Out = AB;}
Labeled Data. In Filament, all non-public data is wrapped in an abstract type Labeled<T, L: Label>, where T is the value type and L is a security label as defined above. 1 2 3 4
pub struct Labeled<T, L: Label> { pub(crate) value: T, pub(crate) _marker: PhantomData<L>, }
Note that Filament employs a phantom-typed field, _marker, to associate security labels with data. This design ensures that labeled values incur no runtime overhead. Furthermore, Filament leverages
Filament : Denning-Style Information Flow Control for Rust AB
1 2
A
B
3
struct A {} struct B {} struct AB {}
1 2
(b) Label types
pub trait Label: Clone + Default + 'static {} pub trait FlowsTo<Target: Label>: Label {}
3 4
Public
11
5 6
impl <L: Label> FlowsTo<L> for L {} impl FlowsTo<AB>for A {} impl FlowsTo<AB>for B {}
(a) Lattice structure (c) Flow encoding Fig. 5. A four-element security lattice. (a) illustrates the lattice hierarchy (ℓ1 ⊑ ℓ2 ). (b) shows the zero-sized types representing security levels. (c) demonstrates the encoding of the FlowsTo relation using Rust’s trait system.
the pub(crate) visibility modifier to enforce opacity of these values, thereby restricting direct access. As a result, labeled values can only be manipulated through the interfaces provided by the Filament library, which are described in subsequent sections. 4.2
Explicit Flows
As introduced in Section 2.2, an explicit flow occurs when an expression 𝑒 is assigned to a variable 𝑥. To enforce IFC, we must ensure that the security label of 𝑥 is at least as restrictive as the label of 𝑒. In a mainstream language like Rust, implementing this enforcement presents two primary challenges: type-system rigidity and annotation burden. The Challenge: Type-System Rigidity. The most significant hurdle in implementing Denning-style IFC within a standard type system is that security-safe flows often appear as type mismatches to the compiler. Consider the following example: 1 2 3 4
let mut x: i32 = 0; // Public let mut y: Labeled<i32, A> = Labeled::new(10); // Secret x = y; // (1) Rejected: Type mismatch y = x; // (2) Rejected: Type mismatch
In assignment (1), Rust correctly prevents a security leak, but it does so because of a structural type mismatch between Labeled<i32, A> and the primitive i32, rather than by detecting an illegal information flow. However, in assignment (2), the same rigidity blocks a perfectly safe flow: moving public data to a secret variable (ℓ𝑃𝑢𝑏𝑙𝑖𝑐 ⊑ ℓ𝐴 ). This highlights a core limitation: a naive type-based approach is often too conservative to distinguish between a dangerous flow (High-to-Low) and a secure one (Low-to-High). To resolve this without intrusive compiler modifications, Filament provides a unified approach using explicit relabeling and automatic inference. Relabeling in Variable Assignment. While a flow from label ℓ to ℓ ′ is secure whenever ℓ ⊑ ℓ ′ , Rust rejects the assignment if ℓ ≠ ℓ ′ . To bridge this gap, we introduce the relabel!(expr, L_target) macro. This macro allows a programmer to explicitly “upgrade” the security label of an expression to satisfy the type system. To ensure soundness, the macro invokes an internal function, __relabel_checked::<_, _, L_target >(...), which statically verifies the flow condition ℓ𝑠𝑟𝑐 ⊑ ℓ𝑡𝑎𝑟𝑔𝑒𝑡 via the L_src: FlowsTo<L_target> trait (Section 4.1). By using relabel!, the programmer reduces the problem of arbitrary lattice flows to a standard, type-safe assignment: 1 2
// Using the relabel! macro to satisfy the type system for line 4 above y = relabel!(x, A); // Success: Static check confirms Public flows to A
12
Jeffrey C. Ching, Quan Zhou, and Danfeng Zhang
This design ensures that label upgrades are explicit, sound, and checked entirely at compile-time. Furthermore, it allows Filament to remain highly permissive while fully leveraging Rust’s existing safety guarantees. Label Propagation via Inference. A key design goal of Filament is to reduce the programmer’s annotation burden, particularly for intermediate expressions such as x + y. While relabel! is necessary for cross-label assignments (partially due to assignment operator overloading is not allowed in Rust), Filament automates label propagation during expression evaluation through operator overloading. When an operation combines two values with labels 𝐿1 and 𝐿2 , Filament automatically computes the resulting label as the lattice join: Labeled<T, Join<L1, L2>>. Because these resulting types are concrete and consistent with the security lattice, Filament leverages Rust’s native type inference engine to determine the labels of intermediate variables. 1 2 3
let x: Labeled<i32, A> = Labeled::new(10); let y: Labeled<i32, B> = Labeled::new(20); let z = x + y; // z is automatically inferred as Labeled<i32, AB>
By utilizing the host language’s inference engine, Filament avoids the need for a specialized external constraint solver, such as the one employed by Jif [3]. This allows for a more ergonomic programming model where explicit information flows are either automatically inferred or easily verified via relabeling. 4.3
Implicit Flows
Challenges. Explicit information flows between data are relatively straightforward to enforce, as type systems inherently check type compatibility between values. However, standard type systems typically do not track the control-flow context, represented by the 𝑝𝑐 label, which is required to enforce implicit flow checks (Section 2.2). Consequently, the primary challenge is to track the 𝑝𝑐 label and incorporate it into type checking without modifying Rust’s underlying type system. One key observation is that when the condition of a branch or loop is public, no additional mechanisms are required. The reason is that public values are represented using ordinary data types without security labels, and all implicit flows within the corresponding control structure are trivially secure because 𝑝𝑐 = ⊥ in this case. For example, consider 1 2 3 4 5
let x: bool = ...; let y: Labeled<int32, A> = Labeled::new(10); if x { y = relabel!(10, A); // both implict flow and explit flow are secure }
It is secure for the the type system to check only explicit flows at line 4 (as described in Section 4.2). This follows because (1) the type system requires the branch condition to be without a label, i.e., public, and (2) the implicit-flow constraint at line 4, 𝑝𝑐 ⊑ A, trivially holds whenever 𝑝𝑐 = ⊥. However, the Rust type system rejects any program whose branch or loop condition is non-public, i.e., has a labeled type, because labeled types are incompatible with the expected type bool. On the positive side, this behavior preserves soundness without requiring additional mechanisms. The remaining challenge, however, is to make the type system more permissive in cases where the branch condition is non-public. To address the challenge, we introduce a novel macro pc_block! to both track 𝑝𝑐 label and check implicit flows within the context. PC Blocks. For any branch or loop whose condition is non-public, Filament requires an explicit annotation using the pc_block! macro. At a high level, pc_block! {(L) {code}} defines a lexical context
Filament : Denning-Style Information Flow Control for Rust
13
in which the program counter label is initialized to ℓ. Within this context, the macro enforces several restrictions: (1) it updates the 𝑝𝑐 label for each branch or loop encountered, (2) it performs implicit-flow checks for every assignment within the block, and (3) it ensures that any function or method call inside the block is free of side effects. We elaborate on each of these restrictions next. Tracking PC Label. The macro pc_block! {(L) {code}} first initializes a local label, __pc, to the annotated label L. When the macro encounters a branch or loop statement, it rewrites the condition using inspect_condition(), which extracts both the underlying boolean value and the security label of the condition. The program counter label is then joined with the condition’s label before entering the branch body via join_labels(__pc, _cond_label), which updates the 𝑝𝑐 for the encountered branch or loop at the type level. The resulting label shadows the outer __pc for the entire scope of the branch. For example, the following code snippet illustrates the computed type-level __pc associated with each branch, assuming that a and b have labels A and B respectively: 1 2 3 4 5 6
pc_block! { (A) { if a { if b { ... } }}}
// label A // label A // label AB // pc reverts to A
Checking Implicit Flows. Every assignment inside pc_block! is rewritten to secure_assign_with_pc, which in addition to the explicit flow checks described in Section 4.2, also verifies that __pc: FlowsTo <L_target>, ensuring that the target label is at least as restrictive than the current 𝑝𝑐. For example, consider the following code snippet: 1 2 3 4 5 6 7 8
let secret: Labeled<bool, A> = ...; let mut x: Labeled<int32, A> = Labeled::new(0); let mut y: Labeled<int32, B> = Labeled::new(0); pc_block! { (A) // pc is set to A if secret { x = relabel!(1, A); // type checking succeeds y = relabel!(1, B); // type checking fails }}
The pc_block! macro enforces implicit-flow checks by verifying the constraint A: FlowsTo<A> at line 6. Since this constraint holds, the assignment at that line is well-typed. In contrast, the check at line 7, A: FlowsTo<B>, fails; consequently, the type system correctly rejects the assignment at line 7. Controlling Side Effects. To control implicit flows via function calls inside a PC block, Filament verifies that such functions are free of side effects. To do so, we follow Cocoon’s implementation of the #[side_effect_free_attr] attribute, and check that only functions with this verified attribute are used inside a PC block. As the verification of the #[side_effect_free_attr] annotation follows the same approach as in Cocoon, we refer interested readers to their paper [20] for further details. Similar to Cocoon, Filament provides an interface, unchecked_operation, as an escape hatch that bypasses all security checks. This interface is intended to address potential imprecision in the verification of the #[side_effect_free_attr] annotation, as well as to support intentional information release via side effects. Similar to declassification interfaces such as declassify(x), the programmer remains responsible for ensuring that the use of such unchecked operations does not introduce unintended information leakage. Notably, we observe that unchecked_operation is not used in any of the case studies presented in our evaluation (Section 5), suggesting that our approach is sufficiently permissive in practice.
14
Jeffrey C. Ching, Quan Zhou, and Danfeng Zhang
pc_block vs. secret_block. While PC blocks in Filament shares certain mechanisms with secret blocks in Cocoon, there are several notable differences. The primary distinction is that pc_block annotations are required only for branches or loops with non-public conditions, whereas secret_block must be applied to any code that manipulates secret values. As a result, we observe a substantial reduction in annotation overhead: Filament requires only 3 PC blocks, compared to 36 secret blocks in Cocoon (Section 5.1). As a consequence, fewer functions requires the #[ side_effect_free_attr] annotations overall. Furthermore, aside from the verification of side-effectfree functions, the additional mechanisms (including tracking PC label and checking implicit flows) enforced by pc_block! are not present in Cocoon. 4.4
Third-Party Security-Agnostic Functions and Methods
Challenges. As discussed in Section 3.3, nontrivial programs routinely depend on the standard Rust library, built-in methods (e.g., .len(), .contains(), and .push()), and third-party libraries (e.g., str::parse). However, these methods and functions are security-agnostic, in the sense that they operate on raw types T rather than labeled types Labeled<T, L>. Hence, programs that manipulate labeled values (e.g., values of type Labeled<String, A>) cannot directly reuse such functions without rewriting them to be label-aware, which is generally infeasible. In the Cocoon programming model, third-party libraries are treated as trusted (i.e., part of the trusted computing base), alongside the Rust compiler and the standard Rust library. Cocoon’s procedural macro maintains an “allowlist” of functions that are deemed side-effect free by its designers. To address the type incompatibility described above, Cocoon adopts the following pattern when invoking trusted libraries: sensitive arguments are first declassified to match the expected function signatures, and the return values are subsequently re-wrapped with appropriate security labels. However, as noted in Section 3.3, this pattern in prone to misuses, as declassified values may bypass all subsequent IFC enforcement mechanisms. In the Filament programming model, we adopt the same threat model: third-party libraries are treated as trusted, alongside the Rust compiler and the standard library. However, to avoid the error-prone patterns employed by Cocoon, Filament treats each function or method in trusted libraries as a black box. In particular, it automatically computes a security label that is at least as restrictive as the labels of all input parameters, and assigns this label to the function’s return value. This behavior is enforced through the macros fcall! and mcall!, which we describe next. Invocation Macros in Filament. Filament introduces the fcall! macro to enable the use of trusted, security-agnostic Rust functions with labeled data. Concretely, the macro operates as follows. First, it generates a sequence of nested __chain or __chain_ref calls, one per argument. Each closure unwraps a Labeled value and binds the underlying data to a fresh variable, thereby exposing only raw values within the innermost scope. Second, at the innermost level, the original function f is invoked on the unwrapped arguments. Third, the result is initially wrapped as Labeled<R, Public>; subsequently, the enclosing __chain calls propagate and join the labels of all arguments via the Join trait. As a result, the final output is associated with the most restrictive label among all input parameters, ensuring that the resulting label conservatively reflects the sensitivity of the inputs. The definition of fcall!(f(a, b)) is shown below: 1 2 3 4 5 6 7
{
use typing_rules::function_rewrite::{SecureChain}; (a).chain(|__v0| { (b).chain(|__v1| { Labeled::<_, Public>::new(f(__v0, __v1)) }) })
Filament : Denning-Style Information Flow Control for Rust
8
15
}
For method calls (e.g., obj.method(args)) and field accesses (e.g., obj.field), both of which require accessing the receiver’s underlying value, Filament introduces the mcall! macro to ensure secure usage. The design of mcall! follows the same general principles as fcall!; however, instead of computing the most restrictive label among all arguments, mcall! preserves the label of the receiver. This design effectively treats each object as a black box for the purposes of information-flow control. Consequently, the result inherits the receiver’s label, ensuring that sensitivity is determined solely by the object being accessed. This is achieved with a label-preserving helper function below: 1 2 3
fn __mcall_preserve_label<T, U, L: Label>(wrapper: &Labeled<T, L>,func: impl FnOnce(&T) → U) → Labeled<U, L> { Labeled::<U, L>::new(func(wrapper.inner())) }
This helper function borrows the underlying value, applies the method or field access within a closure, and wraps the result in a new Labeled value that preserves the original label L. For example: 1 2 3
mcall!(placement.start_row) // Field access // expands to: __mcall_preserve_label(&placement, |inner| inner.start_row)
Furthermore, a single mcall! invocation can express a chain of method calls on a labeled receiver. The macro recursively deconstructs the chain of mcall! expressions to identify the root labeled receiver, and then reconstructs the entire chain as the body of a single closure passed to __mcall_preserve_label. For example: 1 2 3
mcall!(key.chars().all(f)) // expands to: __mcall_preserve_label(&key, |inner| inner.chars().all(f))
The entire call chain is evaluated within the closure on the unwrapped inner value, and only the final result is re-wrapped. As a consequence, intermediate values (e.g., the Chars iterator produced by .chars()) are never individually labeled. This design is sound because the closure boundary ensures that such intermediate values remain unobservable outside the macro, while the final result preserves the label of the original receiver. 4.5
Limitation of Filament
While Filament provides a robust framework for static, lattice-based information flow control, several security dimensions remain outside the current scope of this work. Because Filament enforces IFC statically, security policies are resolved entirely at compile time; consequently, we do not support dynamic labels where the secrecy level of a value changes at runtime [22]. Furthermore, this work focuses strictly on explicit and implicit flows, so side-channel protections (such as timing channels) are not currently addressed. While Filament’s design follows established type-based IFC principles, a formal proof of noninterference for this specific Rust implementation is beyond the scope of this paper. The current design of Filament utilizes a predefined lattice, which simplifies the implementation of the FlowsTo and Join traits but limits the system to policies where the security lattice is static. Additionally, the program counter (𝑝𝑐) label for pc_block! must currently be specified manually by the programmer at each call site. We intend to explore automatic 𝑝𝑐 inference in future iterations to reduce this manual overhead. Moreover, because our pc_block! implementation inherits properties from Cocoon’s secret_block!, only functions within a predefined allowlist can be safely invoked
16
Jeffrey C. Ching, Quan Zhou, and Danfeng Zhang
within these blocks to prevent side effects. A more scalable solution would involve a custom procedural macro to statically verify the side-effect-free nature of arbitrary Rust functions. Finally, Filament’s current model assumes a single-threaded execution context. Extending Filament to handle concurrent Rust, where data-race freedom must be reconciled with information flow across multiple threads, remains an open research challenge. 5
Evaluation
We implement Filament as a library on top of Rust 1.69 to make it directly comparable with Cocoon, which is implemented on the same Rust version. Our implementation consists of about 2000 lines of Rust code. All experiments were conducted on a dual-socket Intel Xeon 6517P server, 251 GB RAM, running Ubuntu 24.04.3 on Rust version 1.69. We open-sourced Filament at [1]2 . To evaluate the usability and performance of Filament, we re-implemented all four applications from the Cocoon code repository, including Calendar, Battleship, Spotify TUI, and Servo, as well as an additional application, JPMail [15], a substantial information flow case study originally implemented in Jif. For each case study, we translate the original Rust code from the Cocoon repository, or the Jif implementation in the case of JPMail, into its Filament equivalent, while enforcing the same IFC policies as in their respective Cocoon and Jif implementations. • Calendar is a simple program that determines the mutual availability of Alice and Bob, where each person’s calendar is considered confidential. • Battleship is a classic two player guessing game in which each player privately places a fleet of ships on a hidden grid. Players take turns guessing coordinates on their opponent’s grid, and the first player to sink all opposing ships wins. This example has been used as a case study in Jif and its extension JRIF [3, 18]. • Spotify TUI is an open-source terminal-based Spotify client written in Rust, allowing users to browse playlists, search for tracks, control playback, and manage their Spotify library entirely from the command line. This application processes user credentials, including user IDs and passwords. So any information derived from or related to the password is treated as confidential. • Servo is Mozilla’s browser engine implemented in Rust. Following the Cocoon implementation, we enforce the same security policy under which JavaScript programs may only access HTTP responses originating from the same server. Responses from different origins are treated as opaque and must not be used exclusively. • JPMail is a secure email system that uses IFC to protect email confidentiality at the language level. It was originally written in Jif, enabling users to send, receive and reply to emails while preserves privacy. The password, content of the email, and Private keys are considered secrets in this application. Across the five case studies, we observe that although Spotify TUI and Servo comprise the largest codebases (11K and 327K LoC, respectively), their security critical components are relatively small. In contrast, smaller applications such as JPMail (2K LoC) require more extensive security annotations due to more intricate security-critical code throughout. Nevertheless, Spotify TUI and Servo illustrate realistic settings in which third party libraries constitute the majority of the codebase. In this section, we address the following research questions. Whenever possible, we also compute the same metrics for the Cocoon equivalents to enable a fair comparison. 2 Anonymized for peer review.
Filament : Denning-Style Information Flow Control for Rust
17
Table 1. System Comparison: LoC and Annotation Density per Tool Original Project Calendar Battleship Spotify TUI Servo JPMail
Filament
Cocoon
LoC
LoC
Label
API
LoC
Label
API
29 286 10,912 327,096 1,894
36 (+24.1%) 293 (+2.4%) 10,966 (+0.5%) 327,160 (+0.02%) 2,006 (+5.9%)
14 16 36 61 199
2 2 23 1 53
48 (+65.5%) 315 (+10.1%) 11,029 (+1.1%) 327,129 (+0.01%) —
0 11 13 64 —
26 23 49 1 —
RQ1 Code Annotation Burden: How much annotation burden is required to enforce IFC with Filament? More specifically, how many security related type annotations and macros are needed to verify IFC policies in Filament? RQ2 Permissiveness: How often must escape hatches, including declassify (excluding intentional uses, such as releasing the mutually available dates of Alice and Bob in the Calendar case study) and unchecked_operation, be used in Filament to bypass security checks when the security enforcement mechanism proves too restrictive in practice? RQ3 Compilation Overhead: What are the compilation time overhead of the IFC enforcement mechanisms? Note that Filament enforces IFC entirely at compile time; consequently, verified Rust programs incur no runtime overhead by design. By re-implementing these examples, we demonstrate that Filament achieves the same security objectives as Cocoon using a principled Denning-style approach while requiring fewer modifications to the original source code. The primary distinction is that Cocoon relies on secret_block! constructs, whereas Filament associates labels directly with individual variables. While variable-level labeling is often perceived to increase the annotation burden, we show that our use of label inference largely mitigates this overhead. Furthermore, the permissive programming model of Filament significantly reduces the number of unnecessary declassification and unchecked operations that can potentially expose secret values to the public. 5.1
Code Annotation Burden
A major concern for any language-based IFC tool is the extent of code modification required for verification, including both security-related type annotations and IFC-library API calls. To estimate the annotation burden associated with Filament and Cocoon, we summarize the total lines of code (LoC) and annotations (categorized into label annotations and API calls) in Table 1. For the first four applications, where the original Rust implementations (without IFC) are available, both Filament and Cocoon exhibit similar LoC, with only minor to modest increases—except for Calendar, due to its small codebase. The additional lines primarily occur at framework boundaries that the label system cannot transparently cross. For example, because the Serialize and Deserialize traits used in Servo are not aware of security types such as Labeled<T, L>, auxiliary helper functions are required in Spotify TUI for both Filament and Cocoon. Nevertheless, the majority of application logic, including UI rendering, protocol parsing, and game loops, remains unchanged. This suggests that, in both systems, annotation effort is localized to security-critical regions. This also explains why the LoC increase is not strictly proportional to the size of the original codebase. For JPMail, originally implemented in Jif with built-in IFC support, we observe a similarly modest increase, likely due to Jif’s use of a customized type system.
18
Jeffrey C. Ching, Quan Zhou, and Danfeng Zhang
Table 2. API usage in Filament Project Calendar Battleship Spotify TUI Servo JPMail
declassify
fcall!/mcall!
pc_block!
relabel!
1 2 7 1 12
0 0 14 0 13
1 0 1 0 1
0 0 1 0 0
Compared to Cocoon, Filament requires fewer lines of code for Battleship (293 vs. 315), Calendar (36 vs. 48), and Spotify TUI (10,966 vs. 11,029), while it is slightly larger for Servo (327,160 vs. 327,129). Overall, Filament implementations tend to be more concise, particularly in the percentage increase over the original code. To better understand the extent of changes introduced by security enforcement, we count the total number of lines containing at least one security-related annotation. These include label annotations at variable declarations and function signatures, as well as uses of Filament interfaces (Figure 4). We apply the same methodology to Cocoon and summarize the results in the “Label” and “API” columns of Table 1. Because Filament adopts a fine-grained, Denning-style approach, a higher number of label annotations is expected. As shown in Table 1, the annotation counts are higher than Cocoon’s for all programs except Servo. Nevertheless, the number of lines requiring security label annotations in Filament remains low in practice, with only 16 lines for Battleship, 36 for Spotify TUI, and 61 for Servo. Only JPMail incurs a substantially higher burden, as many data sources must be labeled as secret and a large portion of its codebase is security-critical. Overall, the label annotation burden in Filament is moderate at most; this is notable given that Filament enforces both explicit and implicit flows at the expression level while fully leveraging Rust’s inference engine. A clear strength of Filament compared to Cocoon is the significant reduction in IFC library API calls. The permissive programming model of Filament completely eliminates the need for Cocoon’s secret_block!. Consequently, this reduces: (1) the necessity for frequent declassification calls and attribute tags; and (2) the repetitive overhead of wrap and unwrap calls within every secret_block!, as discussed in Section 3.1. The API calls in Filament consist mainly of macros like fcall! and mcall! to interact with third-party libraries, along with several #[side_effect_free_attr] attributes for functions executed under PC blocks. A breakdown for each application is shown in Table 2. Across all four applications, the annotation burden for Filament remains low: Battleship uses only 2 API calls, while Spotify TUI requires 23 (7 declassify, 14 fcall!/mcall!, 1 relabel!, and 1 pc_block!). Calendar and Servo require the least instrumentation. JPMail is the most annotation-heavy, with 12 declassification calls reflecting its complex multi-principal security policy; these calls occur mostly at the socket interface. The fcall! and mcall! macros propagate labels through function calls without requiring manual argument declassification, reducing the total annotation count compared to a block-based approach. Another factor contributing to the reduced API call count is Filament’s more permissive programming model, which avoids the need for spurious escape hatches (such as unchecked_operation and declassify) required by Cocoon to bypass security checks. We elaborate on this point in the following discussion.
Filament : Denning-Style Information Flow Control for Rust
5.2
19
Permissiveness
As discussed in Section 3.1 and Section 3.3, a limitation of the Cocoon programming model is that programmers are sometimes required to use escape hatches, such as unchecked_operation and declassify, either to circumvent checks that are overly restrictive in practice or to accommodate coding patterns necessary for reusing third-party libraries. To better understand the frequency and underlying reasons for these escape hatches, we measure the number of invocations for these APIs. Additionally, we count the number of pc_block! and secret_block! instances in Filament and Cocoon, respectively. The results are summarized in Table 3. Table 3. API usage comparison: Filament vs. Cocoon. Filament
Cocoon
Project
D
U
P
D
U
S
Calendar Battleship Spotify TUI Servo
1 2 7 1
0 0 0 0
1 0 1 0
1 2 17 1
0 2 0 0
17 4 15 0
APIs: D–declassify, U–unchecked_operation, P–pc_block!, S–secret_block!
The unchecked_operation API, which completely bypasses all security checks in both Cocoon and Filament, is used twice in Cocoon’s implementation of Battleship, whereas the Filament implementation does not require it. This difference arises because Filament’s Denning-style analysis eliminates unnecessary secret blocks, thereby avoiding superfluous side-effect checks on certain functions, as illustrated in Figure 1b. Figure 6a shows another case where Cocoon’s random function requires unchecked_operation because it is used within another function tagged with #[ side_effect_free_attr] (random_maybe_illegal_placement), which is used in a secret block. Filament avoids this issue because Filament can distinguish implicit flows from explicit ones, and no pc block is required in the Battleship application. Hence, no side effect checks are required. Although only two instances of unchecked_operation appear across the four applications in the Cocoon repository, this scarcity is likely due to either the small scale of two applications (Battleship and Calendar) or a reliance on trusted third-party libraries (Spotify TUI and Servo), which eliminates the need for side-effect checks under the assumed threat model. For larger applications such as JPMail, we expect patterns similar to those in Battleship to occur more frequently, leading to a greater reliance on unchecked_operation. In contrast, Filament mitigates this limitation by explicitly checking information flows between secret data and target sinks, requiring unchecked_operation only when a function with side effects is invoked within a sensitive branch. The second escape hatch is declassify, available in both tools. Since intentional declassification is required in many applications (e.g., releasing mutually available dates in Calendar), we manually examined all 11 occurrences of declassify in the Filament implementations. We find that all such uses are intentional and necessary for application functionality. In contrast, Cocoon’s 10 additional uses (all within Spotify TUI) are unnecessary, potentially exposing secret values to the public. We have already discussed a representative example of this category in Figure 3. We attribute the increased permissiveness of the Filament programming model primarily to the significant reduction in secret blocks compared to Cocoon. In total, 36 secret blocks are used across the Cocoon applications. Because Cocoon does not distinguish between explicit and implicit flows, IFC enforcement within these blocks must be conservative, disallowing side effects to prevent implicit flows. In contrast, Filament eliminates the need for secret blocks by design, applying
20 1 2 3 4
Jeffrey C. Ching, Quan Zhou, and Danfeng Zhang #[side_effect_free_attr] pub fn random(limit: usize) → usize { unchecked_operation(rand::thread_rng().gen_range(0..limit)) }
5 6 7 8 9 10 11 12 13
#[side_effect_free_attr] fn random_maybe_illegal_placement(grid: &Grid<bool>, ship: &Ship) → Placement { let orientation = util::random(2); if orientation == 1usize { /* ... */ } else { /* ... */ } let row = util::random(row_limit); let col = util::random(col_limit); Placement { /* ... */ } }
(a) random function in Cocoon, utilizing unchecked_operation. 1 2 3
pub fn random(limit: usize) → usize { rand::thread_rng().gen_range(0..limit) }
4 5 6 7
fn random_maybe_illegal_placement(grid: &Grid<bool>, ship: &Ship) → Placement { /* ... same logic ... */ }
(b) random function in Filament, without unchecked_operation. Fig. 6. Comparison of the random function implementation in the Battleship case study.
similar restrictions only within pc_block!. Notably, this construct is required only for branches conditioned on sensitive values and is used only once in Spotify TUI. A second contributing factor is the introduction of the mcall!, fcall!, and relabel! macros, which eliminate the need to declassify labeled parameters when invoking third-party library functions. Moreover, because Rust supports label inference, Filament does not require wrapping all secret computations within a single block, allowing the code to follow the original structure faithfully. Across our case studies, we wrap sensitive values in Labeled<T, L> upon declaration and propagate them using our macros to enforce label-safe operations. Explicit declassify calls are inserted only where the logic genuinely requires revealing secret data, and pc_block! is utilized only when control flow branches on secret values. 5.3
Compilation Overhead
Since Filament relies on procedural macros, it generates auxiliary code that must be processed by the compiler. In particular, pc_block! produces a dual path expansion similar to Cocoon to check if there is information leak through implicit flow statically, while fcall! and mcall! introduce additional scaffolding to mediate library calls. Although these constructs are eliminated during optimization, they still need to be parsed and type checked. Accordingly, we evaluate whether such expansions have a significant impact on compilation time and compare the performance of Filament with that of Cocoon. To evaluate this overhead, we measured median build times for each project. Table 4 reports the results for clean builds. The data demonstrates that Filament’s instrumentation introduces negligible overhead for large, dependency-heavy projects. Although Battleship and Calendar exhibit a more
Filament : Denning-Style Information Flow Control for Rust
21
Table 4. Compilation time comparison: Filament vs. Cocoon (relative to baseline) Baseline Project Spotify TUI Servo Battleship Calendar
Filament
Cocoon
Median (s)
Median (s)
Overhead
Median (s)
Overhead
22.20 193.86 4.69 4.14
22.30 189.36 5.15 4.25
+0.45% –2.32% +9.81% +2.66%
22.43 195.56 5.71 4.97
+1.04% +0.88% +21.75% +20.05%
noticeable relative overhead, we attribute this to their small baselines. For example: Battleship has few external dependencies, the fixed cost of compiling the IFC library crates (macros and typing_rules) represents a larger share of the total build time. Conversely, for Spotify TUI and Servo, this fixed cost is amortized over the compilation of heavyweight dependencies, making the overhead nearly unmeasurable. Spotify TUI shows a negligible difference (0.45%), while Servo compiles slightly faster under Filament (−2.32%), a variance we attribute to build-cache fluctuations rather than a genuine speedup. These results, shown in Table 4, confirm that Filament imposes minimal compilation overhead. Despite using a more granular Denning-style approach, the overhead remains lower than that of Cocoon in all cases. This suggests that the overhead scales with the ratio of IFC library compilation to the total build time rather than with the volume of annotated code. Consequently, as a project grows in complexity, the relative overhead of adopting Filament diminishes further. 6
Related Work
Granularity of IFC. The distinction between fine-grained and coarse-grained systems represents a fundamental design choice in IFC. Fine-grained type systems, such as Jif [24] and FlowCaml [35], track security labels at the level of variables and expressions. In contrast, coarse-grained systems, commonly used in IFC operating systems [19, 40], associate labels with larger entities such as subjects and objects (e.g., processes and files). Several Haskell-based IFC systems built on the LIO model [6, 14, 26, 36, 37] adopt an intermediate approach by tracking labels at the granularity of code blocks, which we refer to as block-level IFC in this paper. Although Cocoon is implemented in Rust, it conceptually also provides block-level IFC (Section 2.3). The choice of granularity has been widely studied in the IFC literature. Rajani et al. [28] identify granularity as a key factor in the design of IFC type systems. In subsequent work [29], they show that static fine-grained and static coarse-grained systems are equally expressive despite their structural differences, providing both a formal semantics and a type-preserving translation between the two. Similar discussions have arisen in the context of dynamic IFC for systems and programming languages [31, 36]. This line of work culminates in Vassena et al. [38], which demonstrates that fine-grained and coarse-grained dynamic systems are also equally expressive. Although fine-grained and coarse-grained IFC systems are theoretically equivalent in expressiveness, the choice of granularity in a programming model remains an important design consideration. As argued throughout this paper, developing IFC-enabled programs in Filament is more intuitive and natural for programmers. Moreover, the resulting code remains closer to conventional Rust code written without IFC, which facilitates porting existing Rust projects to Filament. IFC Tools and Application. Prior IFC tools span both language extensions and library-based approaches. Early systems such as Jif [3] and Flow Caml [35] provide fine-grained IFC for Java-like and OCaml-like languages, respectively, by extending their compilers and type systems. While
22
Jeffrey C. Ching, Quan Zhou, and Danfeng Zhang
these designs offer strong security guarantees, they rely on nonstandard compilation toolchains, which has limited the practical adoption of these otherwise well-founded techniques. To improve accessibility for programmers, subsequent research explored embedding IFC frameworks directly within existing programming languages. Many of these efforts target functional languages, as they have expressive built-in type systems. For example, Haskell-based systems like LIO (Labeled IO) [36] and HLIO [6] enforce dynamic IFC through a security monad. In these designs, security labels are associated with monadic computations rather than individual values, an approach initially explored by Li and Zdancewic [21] and later simplified in Russo’s lightweight Haskell IFC library [33], where sensitivity is tracked at the boundaries of monadic blocks. More recent work has extended this line of research by incorporating stronger static guarantees. For instance, Lifty [26] integrates the LIO model with liquid types to statically verify IFC policies and automatically repair policy violations. Similarly, DepSec [13] demonstrates that dependently typed languages such as Idris can enforce data-dependent security policies entirely at the type level. Besides functional settings, researchers have also explored embedding IFC directly within existing imperative programming languages. One common approach is to extend existing compilers with an information-flow analysis pass that tracks dependencies and enforces security policies during compilation. Representative systems following this strategy include Flowistry [8], Pidgin [16], FlowFence [12], and CtChecker [41]. However, such systems require customized compilers, making them less compelling for end users. Moreover, maintaining customized compilers to keep pace with the evolution of their underlying base languages can be both costly and time-consuming. More recently, Cocoon [20] and its successor Carapace [4], which Filament is inspired by, present the first static IFC systems that work with a mainstream imperative language without modifying the compiler. As discussed in Section 2.3, both systems provide block-level IFC, whereas Filament supports Denning-style, fine-grained IFC. Carapace additionally supports dynamic labels, a feature that is currently absent in Filament. This represents an orthogonal direction that we plan to explore in future extensions of Filament. 7
Conclusion and Future Work
We presented Filament, a Denning-style static information-flow control (IFC) library for Rust that requires no compiler modifications. In contrast to block-level IFC approaches such as Cocoon, Filament enforces both explicit and implicit flows at the granularity of expressions and variables. This design allows values at various security labels to coexist within the same scope while still ensuring end-to-end security through Denning-style IFC enforcement. Through its novel design, Filament addresses three key challenges in constructing a practical IFC library for Rust. First, it enforces explicit-flow checks at the granularity of expressions and variables, yielding a more permissive programming model without requiring substantial code rewriting compared to prior work, while also reducing manual annotations by leveraging Rust’s type inference system. Second, the novel pc_block! construct enables implicit-flow enforcement, a defining feature of Denning-style IFC systems, that is absent in prior approaches without compiler modifications. Third, the fcall! and mcall! macros provide seamless interoperability with the standard library and third-party functions, without introducing error-prone patterns that are susceptible to misuse. Our evaluation demonstrates that Filament incurs negligible compilation overhead and requires only modest annotation effort, particularly in programs that heavily depend on external libraries. Furthermore, Filament offers a more permissive programming model than Cocoon: implementations written using Filament rely less frequently on escape hatches that bypass security checks compared to their Cocoon counterparts.
Filament : Denning-Style Information Flow Control for Rust
23
For future work, we plan to extend Filament to support dynamic IFC policies, in which the sensitivity and integrity of data may evolve over time. We also aim to investigate the scalability of Filament to larger codebases and to explore whether its macro-based design can be further streamlined through tighter integration with Rust’s procedural macro ecosystem. Data Availability Statement An initial artifact for Filament consists of the core IFC library and the complete source code for the examples discussed in this paper. The artifact is currently compatible with Rust 1.69, with support extending up to Rust 1.83. Please note that compilation times may vary depending on the hardware specifications of the host machine. We intend to submit the full artifact for Artifact Evaluation. A temporary version of the source code, including the implementation of both Filament and the examples is available at the following link [1]. References [1] [n. d.]. Filament Implementation. https://github.com/jeffreyccching/filament-ifc-proto [2] 2024. Cocoon-implementation. https://github.com/PLaSSticity/Cocoon-implementation/. [3] 2026. Jif: Java + Information Flow. https://www.cs.cornell.edu/jif/. Accessed: 2026-03-13. [4] Vincent Beardsley, Chris Xiong, Ada Lamba, and Michael D Bond. 2025. Carapace: Static–Dynamic Information Flow Control in Rust. Proceedings of the ACM on Programming Languages 9, OOPSLA1 (2025), 364–392. [5] D Elliot Bell and Leonard J LaPadula. 1973. Secure computer systems: Mathematical foundations. Technical Report. [6] Pablo Buiras, Dimitrios Vytiniotis, and Alejandro Russo. 2015. HLIO: Mixing static and dynamic typing for informationflow control in Haskell. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming. 289–301. [7] Michael R. Clarkson, Stephen Chong, and Andrew C. Myers. 2008. Civitas: Toward a Secure Voting System. In 2008 IEEE Symposium on Security and Privacy (SP 2008). IEEE, Oakland, CA, USA, 354–368. [8] Will Crichton, Marco Patrignani, Maneesh Agrawala, and Pat Hanrahan. 2022. Modular information flow through ownership. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 1–14. [9] Dorothy E Denning. 1976. A lattice model of secure information flow. Commun. ACM 19, 5 (1976), 236–243. [10] Dorothy E Denning and Peter J Denning. 1977. Certification of programs for secure information flow. Commun. ACM 20, 7 (1977), 504–513. [11] Petros Efstathopoulos, Maxwell Krohn, Steve VanDeBogart, Cliff Frey, David Ziegler, Eddie Kohler, David Mazieres, Frans Kaashoek, and Robert Morris. 2005. Labels and event processes in the Asbestos operating system. ACM SIGOPS Operating Systems Review 39, 5 (2005), 17–30. [12] Earlence Fernandes, Justin Paupore, Amir Rahmati, Daniel Simionato, Mauro Conti, and Atul Prakash. 2016. {FlowFence}: Practical data protection for emerging {IoT} application frameworks. In 25th USENIX security symposium (USENIX Security 16). 531–548. [13] Simon Gregersen, Søren Eller Thomsen, and Aslan Askarov. 2019. A dependently typed library for static informationflow control in Idris. In International Conference on Principles of Security and Trust. Springer, 51–75. [14] Stefan Heule, Deian Stefan, Edward Z Yang, John C Mitchell, and Alejandro Russo. 2015. IFC inside: Retrofitting languages with dynamic information flow control. In International Conference on Principles of Security and Trust. Springer, 11–31. [15] Boniface Hicks, Kiyan Ahmadizadeh, and Patrick McDaniel. 2006. From languages to systems: Understanding practical application development in security-typed languages. In 2006 22nd Annual Computer Security Applications Conference (ACSAC’06). IEEE, 153–164. [16] Andrew Johnson, Lucas Waye, Scott Moore, and Stephen Chong. 2015. Exploring and enforcing security guarantees via program dependence graphs. ACM SIGPLAN Notices 50, 6 (2015), 291–302. [17] Elisavet Kozyri, Owen Arden, Andrew C Myers, and Fred B Schneider. 2019. JRIF: reactive information flow control for java. In Foundations of Security, Protocols, and Equational Reasoning: Essays Dedicated to Catherine A. Meadows. Springer, 70–88. [18] Elisavet Kozyri and Fred B Schneider. 2020. RIF: Reactive information flow labels. Journal of Computer Security 28, 2From dynamic to static and back: Ridi (2020), 191–228.
24
Jeffrey C. Ching, Quan Zhou, and Danfeng Zhang
[19] Maxwell Krohn, Alexander Yip, Micah Brodsky, Natan Cliffer, M Frans Kaashoek, Eddie Kohler, and Robert Morris. 2007. Information flow control for standard OS abstractions. ACM SIGOPS Operating Systems Review 41, 6 (2007), 321–334. [20] Ada Lamba, Max Taylor, Vincent Beardsley, Jacob Bambeck, Michael D Bond, and Zhiqiang Lin. 2024. Cocoon: Static Information Flow Control in Rust. Proceedings of the ACM on Programming Languages 8, OOPSLA1 (2024), 166–193. [21] Peng Li and Steve Zdancewic. 2006. Encoding information flow in Haskell. In 19th IEEE Computer Security Foundations Workshop (CSFW’06). IEEE, 12–pp. [22] Peixuan Li and Danfeng Zhang. 2022. Towards a General-Purpose Dynamic Information Flow Policy. In 2022 IEEE 35th Computer Security Foundations Symposium (CSF). IEEE, Haifa, Israel, 260–275. [23] Jed Liu, Michael D George, Krishnaprasad Vikram, Xin Qi, Lucas Waye, and Andrew C Myers. 2009. Fabric: A platform for secure distributed computation and storage. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles. 321–334. [24] Andrew C Myers. 1999. JFlow: Practical mostly-static information flow control. In Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 228–241. [25] Andrew C Myers and Barbara Liskov. 1997. A decentralized model for information flow control. ACM SIGOPS Operating Systems Review 31, 5 (1997), 129–142. [26] Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, and Armando Solar-Lezama. 2020. Liquid information flow control. Proceedings of the ACM on Programming Languages 4, ICFP (2020), 1–30. [27] François Pottier and Vincent Simonet. 2002. Information flow inference for ML. In Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 319–330. [28] Vineet Rajani, Iulia Bastys, Willard Rafnsson, and Deepak Garg. 2017. Type systems for information flow control: The question of granularity. ACM SIGLOG News 4, 1 (2017), 6–21. [29] Vineet Rajani and Deepak Garg. 2018. Types for information flow control: Labeling granularity and semantic models. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF). IEEE, 233–246. [30] Vineet Rajani and Deepak Garg. 2020. On the expressiveness and semantics of information flow types. Journal of Computer Security 28, 1 (2020), 129–156. [31] Indrajit Roy, Donald E Porter, Michael D Bond, Kathryn S McKinley, and Emmett Witchel. 2009. Laminar: Practical finegrained decentralized information flow control. In Proceedings of the 30th ACM SIGPLAN conference on programming language design and implementation. 63–74. [32] Alejandro Russo. 2015. Functional pearl: two can keep a secret, if one of them uses Haskell. ACM SIGPLAN Notices 50, 9 (2015), 280–288. [33] Alejandro Russo, Koen Claessen, and John Hughes. 2008. A library for light-weight information-flow security in Haskell. ACM Sigplan Notices 44, 2 (2008), 13–24. [34] Andrei Sabelfeld and Andrew C. Myers. 2003. Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21, 1 (January 2003), 5–19. [35] Vincent Simonet. 2003. The flow caml system. Software release. Located at http://cristal. inria. fr/˜ simonet/soft/flowcaml 116 (2003), 119–156. [36] Deian Stefan, Alejandro Russo, John C. Mitchell, and David Mazières. 2011. Flexible Dynamic Information Flow Control in Haskell. In Proceedings of the 4th ACM Symposium on Haskell. ACM, Tokyo, Japan, 95–106. [37] Marco Vassena, Alejandro Russo, Pablo Buiras, and Lucas Waye. 2018. Mac a verified static information-flow control library. Journal of logical and algebraic methods in programming 95 (2018), 148–180. [38] Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, and Deian Stefan. 2019. From fine-to coarse-grained dynamic information flow control and back. Proceedings of the ACM on Programming Languages 3, POPL (2019), 1–31. [39] Dennis Volpano, Cynthia Irvine, and Geoffrey Smith. 1996. A sound type system for secure flow analysis. Journal of computer security 4, 2-3 (1996), 167–187. [40] Nickolai Zeldovich, Silas Boyd-Wickizer, and David Mazieres. 2008. Securing Distributed Systems with Information Flow Control.. In NSDI, Vol. 8. 293–308. [41] Quan Zhou, Sixuan Dang, and Danfeng Zhang. 2024. CtCheker: A Precise, Sound and Efficient Static Analysis for Constant-Time Programming. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 46–1.