data types (in short ADTs) serve as a fundamenWorkshop Proceedings
The security of various cryptographic constructions relies on unique or even unpredictable values. Examples include nonces in cryptographic protocols, initialization vectors in modes of symmetric encryption, salts in password-based key derivation functions and others. These values are often generated as a random numbers of prescribed length.
Programmers who are not experts in cryptography
might assume that it is not strictly necessary to generate
a new random number every time. Some of them may be
lazy and provide fixed numeric constant instead of a new
random number for each use. After all, the cryptographic
construction will “correctly”1 work even with this fixed
numeric constant. However, if the no-reuse principle is
not followed, it can lead to a serious security vulnerability
in the resulting application (which is not visible at first
glance). A well-known example of this issue is “forbidden
attack” for AES-GCM [
In this paper, we propose a method which demonstrate how to implement a cryptographic library that would allow the compiler to detect incorrect (i.e. repeated) use of such one-time random numbers at compile time. We will divide this task into two main parts:
pecting a random number gets as an argument a random number generated by an “approved” method. E.g. a true random number generated by a specialized hardware device and not just some pseudorandom number generated by weak CEUR algorithm. Alternatively, we can enforce the use of a specific, vetted software implementation.
generated random number is used, it cannot be reused for the second time.
Substructural type systems which enforce single (or at most single) use semantics on values, can be utilized for this purpose. This approach can be applied not only to languages that support linear (single use) types but also to any language with similar features, such as ownership and borrowing in Rust, afine types in Haskell, or uniqueness types in Clean. We will illustrate this concept using the Rust programming language.
In Section 2, we describe the key features of abstract data types necessary to enforce proper random number generation. Next, in Section 3, we introduce the fundamental concepts of substructural type systems, focusing on linear and afine type systems that provide strict control over resource usage, which we utilize to prevent the reuse of random numbers. In Section 4, we then explore the unique features of the Rust programming language, including traits, ownership, move semantics, and borrowing rules, which we leverage to implement the nonce module. Finally, in Section 5, we demonstrate how to use the nonce module in a cryptographic library to enforce correct nonce usage.
CEUR
ceur-ws.org
CEUR
Workshop Proceedings (CEUR-WS.org)
a formal specification for data types that decouples their PWroorckeshdoinpgs ISN1613-073 1Depending on the cryptographic construction, it might (for exam- behavior from their concrete implementation. ADTs are ple) still correctly encrypt and decrypt messages. defined by their external behavior, such as operations like 1 mod nonce { 2 // A public struct with a private 3 // random value of type u128 pub struct Nonce { val: u128, insertion and deletion, while concealing the underlying implementation details from the user. This encapsulation grants implementers the flexibility to employ any internal data structures or modify their approach in the future. 4 As long as the external behavior (interface) remains con- 5 sistent, existing code utilizing the ADT will continue to 6 } function without requiring modifications to accommo- 7 date changes in the internal implementation. In this way 8 impl Nonce { ADTs also promote software reuse and modularity. 9 // A public constructor method
ADTs are widely used and supported in many standard 10 pub fn new() -> Nonce { programming languages, including C++, Java, or Pascal. 11 use rand::prelude::*; They are typically realised as modules or objects that 12 Nonce { val: random() } hide internal implementation details and expose only the 13 } public interface to the client. For instance, if we want to 14 implement a stack (a LIFO data structure) as an ADT, we 15 // A public getter method would provide public functions such as push, pop, and 16 pub fn get(self: &Self) -> &u128 { others and a type Stack for variables holding values of 17 &self.val this ADT. But the important aspect is, that we do not 18 } disclose to the client any information on how the stack 19 } is internally implemented. It could be a linked list, an 20 array, or something totally diferent. For example, if a 21 // The Copy and Clone traits are more eficient data structure becomes available, the inter- 22 // intentionally not implemented nal implementation of the ADT can be updated without 23 afecting the client code, as long as the public interface 24 // DerefMut is needed to modify through remains unchanged. Additionally, we also do not pro- 25 // a dereference, so since only Deref vide any external means for creating a new stack (since 26 // is defined, nonce cannot be modified external users lack knowledge of the internal details of 27 use std::ops::Deref; the Stack type). The only way to create a new stack is 28 impl Deref for Nonce { to call a function from the module, which returns a new 29 type Target = u128; Stack value (or to create a new instance if objects are 30 fn deref(self: &Self) -> &u128 { used instead of modules). 31 &self.val
ADT are particularly useful for constraining access 32 } and preventing invalid states. By defining the stack as 33 } ADT, the module implementer can maintain strict con- 34 } trol over its representation. Clients cannot accidentally or intentionally alter any of the stack’s representation Listing 1: Implementation of nonce module in Rust invariants. This ensures that the stack remains in a valid state, and its operations behave as expected. Therefore ADTs enhance code maintainability and readability. While abstract types are a powerful means of con
We can use this technique to create a nonce module trolling the structure and creation of data, they are not in the Rust programming language with Nonce abstract suficient to limit the ordering and number of uses of data type (see Listing 1). values and functions. As another example, we can men
We have defined a public struct type Nonce in Rust, en- tion e.g. files. There is no (static) way to prevent a file
capsulating a private random value of type u128. Direct from being read after it has been closed [
Since the client needs to call the new method, we can by using ADTs alone. However, this can be enforced ensure that on line 12, we, as implementers, select the in programming languages that support the appropriate appropriate system function to generate a new random substructural type system. number. This could potentially involve using a hardware RNG for added security. However, to keep this example simple, this step is not included.
context
⏞Γ⏞1⏞⏞,⏞∶⏞⏞⏞⏞⏞⏞,⏞⏞∶⏞⏞⏞⏞⏞⏞,⏞Γ⏞2 ⊢ ∶
Before presenting our proposed solution using
substructural type system, it’s essential to provide a brief overview ⏟Γ⏟1⏟⏟,⏟∶⏟⏟⏟⏟⏟⏟,⏟⏟∶⏟⏟⏟⏟⏟⏟,⏟Γ⏟2 ⊢ ∶ (Exchange)
of what substructural type systems are [
Linear and afine type systems are a special case of sub- extra, unneeded assumptions to the context, does not structural type systems. They are particularly beneficial prevent a term from type checking. in scenarios where strict control over resource usage is crucial and we need a way for constraining usage of the Γ ⊢ ∶ (Weakening) interface of this resource (imagine resources like files or Γ, ⏟∶ ⊢ ∶ memory). By utilizing linear (or afine) types, we can en- unneeded assumption sure that certain values or operations are used exactly (or Finally, the third property, contraction, states that if we at most) once and in some way in the correct sequence, can type check a term using two identical assumptions thereby preventing common programming errors and en- ( 2 ∶ and 3 ∶ ) then we can check the same term hancing the security and reliability of software systems. using a single assumption.
In the context of our forthcoming solution, we will demonstrate how substructural type system in Rust enable us to enforce the one-time use of random numbers, Γ, 2 ∶ , 3 ∶ ⊢ ∶ (Contraction) thereby mitigating potential security vulnerabilities as- Γ, 1 ∶ ⊢ [ 2 ↦ 1, 3 ↦ 1] ∶ sociated with nonce reuse in cryptographic applications.
This approach not only leverages Rust’s robust type
system but also showcases the practical application of
advanced type theories in real-world software development.
3.1. Structural Properties
In accordance with Pierce’s work [
The comma operator (,) serves to append a pair to the end of the type-checking context (e.g. Γ1, ∶ ), or to concatenate two type-checking contexts (e.g. Γ1, Γ2). Let us denote by Γ ⊢ ∶ that, within the context Γ, we can type-check that the term has the type .
We denote the substitution of the term for the free variable in the term by [ ↦ ] . We assume that and have the same type, ensuring that the resulting term [ ↦ ] is also correctly typed (in simply-typed lambda calculus). Instead of writing [ 3 ↦ 4]([ 1 ↦ 2]) , we use the more concise form [ 1 ↦ 2, 3 ↦ 4] .
premise conclusion
Finally, by typing rule we mean that if its premise is true, then we can conclude that its conclusion also holds.
Lets discuss three basic structural properties. The first property, exchange, indicates that the order in which we write down variables in the context is irrelevant. A corollary of exchange is that if we can type check a term with the context Γ, then we can type check that term with any permutation of the variables in Γ.
(Typing rule)
In his book [
His book provides an in-depth discussion on the
principles of substructural type systems and their applications,
making it an valuable resource for those looking to delve
deeper into this topic.
3.2. Substructural Type Systems
A substructural type system is any type system that is
designed so that one or more of the structural properties
do not hold [
Linear type systems ensure that every variable is used exactly once by allowing exchange but not weakening or contraction.
Afine type systems ensure that every variable is used at most once by allowing exchange and weakening, but not contraction.
Relevant type systems ensure that every variable is used at least once by allowing exchange and contraction, but not weakening.
Ordered type systems ensure that every variable is used exactly once and in the order in which it is introduced. Ordered type systems do not allow any of the structural properties.
The Fig. 1 below2 can serve as a mnemonic for the In Rust, there are several important standard traits relationship between these systems. The system at the that provide foundational functionality and are widely bottom of the diagram (the ordered type system) admits used. For the purposes of this paper, it is important to no structural properties. As we proceed upwards in the understand, that the Copy and Clone traits allow for dudiagram, we add structural properties: E stands for ex- plication of value. Therefore, we do not implement them change; W stands for weakening; and C stands for con- for the Nonce. The Deref trait only allows for reading a traction. stored value. To enable writing, the DerefMut trait is necessary, which we also do not implement. Programmers unrestricted (E,W,C ⇒ structural) can access the stored u128 value using the nonce.get() +C +W method or by dereferencing with *nonce. Both return an immutable reference (as in immutable borrowing). afine (E,W)
relevant (E,C) +W
+C linear (E)
+E
ordered (none)
4.2. Ownership rules
In Rust, when a value is assigned to a variable, the
variable becomes the “owner” of that value. When the owner
variable goes out of scope, the value is automatically
deallocated. Rust enforces that there can only be one owner
for a value at a time. This is the essence of substructural
type system in Rust [
be dropped (memory will be deallocated).
4.3. Move semantics
All type systems below unrestricted (aka. structural)
are called substructural type systems. It might be
possible to define type systems containing other
combinations of structural properties, such as contraction only
or weakening only, but so far researchers have not found
applications for such combinations [
Move semantics in Rust is a fundamental concept that
allows the transfer of ownership of a value from one
variable to another. When a value is assigned from one
variable to another (e.g. let s2 = s1;) or passed to
a function, ownership of the value is transferred (aka
4. Rust moved) from s1 to the new variable s2 unless the value
implements the Copy trait [
• Immutable borrowing:
You can have multiple immutable references to a value, but you cannot modify the value through these references. This prevents data races because multiple threads can read a value without the risk of it being modified simultaneously. • Mutable borrowing:
You can have only one mutable reference to a value, and no other references (mutable or immutable) can coexist with it. This enforces exclusive access to the value, ensuring that only one part of the code can modify it at a time. println!("{}, world!", s1); //error: val. borrowed ^^ here after move let s2 = s1; // value moved from s1 to s2 stack
s1 ptr len capacity
s2 ptr len capacity 5 5 5 5
heap index value 0 1 2 3 4 h e l l o
On Listing 3 we implement function need_new_ random_u128_every_time to demonstrate function signature for functions that require fresh random value for Listing 2: Classical example of ownership rules every call. The body of the function is not significant, but we demonstrate, that the nonce value can be used
We will demonstrate some of these rules on Listing 2. repeatedly inside library implementation, which is often
On line 2 we create a string and assign its value into needed. We also implement Deref trait, so * can be used
variable s1. This variable is now the only owner of the on line 10 instead of longer nonce.get() from line 7.
string. Then on line 6 we move value from variable s1
to new owner – variable s2 (because String does not 1 fn need_new_random_u128_every_time(
implement Copy trait). Now s2 is the only owner of 2 nonce: nonce::Nonce
the string value. That is the reason, why we can not 3 ) {
use variable s1 on line 8 to borrow the string value to 4 let _tmp = nonce.get();
println! function. But we could use s2 for this. When 5
s2 comes out of scope the string value can be deallocated 6 println!("Nonce param value: {}",
from memory. This is illustrated in Fig. 2 on the right3. 7 nonce.get());
After assigning to s2 the value from s1, variable s2 points 8
to the same memory on the heap, but s1 can not be used 9 println!("Nonce param value: {}",
for dereferencing anymore. This is used primarily for 10 *nonce);
memory management without the need for a garbage 11 }
collector or explicit deallocation. For more see e.g. [
The solution in Rust is syntactically very simple because is cWalhleedn,ftuhnecntivoanluneeeodw_nneerws_hriapnidsomm_ouv1ed28f_roemvetrhye_ tloicmael it is well aligned with Rust syntax. Usually, when func- variable to the argument and thus local variable can not tions in Rust take arguments, they are passed as refer- be used anymore. As an example, if in Listing 4 we ences (with & before variable name). This way value is comment out line 7, we will get compile time error “value not moved to the parameter from the local variable (it is used here after move” on the next line. just borrowed). However, we can prevent borrowing by not taking reference as the argument and not implementing Copy trait in Nonce type.
Listing 3: Example of function with nonce as argument
We have demonstrated how to use abstract data types and substructural type systems for enforcing the freshness of 1 fn main() { 2 // Structs with private fields can be 3 // created only using public constructors 4 let mut nonce = nonce::Nonce::new(); 5 need_new_random_u128_every_time(nonce); 6 7 nonce = nonce::Nonce::new(); 8 need_new_random_u128_every_time(nonce); 9 10 need_new_random_u128_every_time( 11 nonce::Nonce::new() 12 ); 13 }
Listing 4: Example of nonce usage nonces for cryptographic library function calls. In Rust, the syntax is very straightforward. This solution can be implemented also in other languages with afine or linear type system, like Haskell, which experimentally supports linear types from version 9.0.1. But syntax, in this case, is not so clear as in Rust.
This publication is the result of support under the Operational Program Integrated Infrastructure for the project: Advancing University Capacity and Competence in Research, Development a Innovation (ACCORD, ITMS2014+:313021X329), co-financed by the European Regional Development Fund.