=Paper=
{{Paper
|id=Vol-3792/paper25
|storemode=property
|title=Enforcing Fresh Nonces with Affine Type System
|pdfUrl=https://ceur-ws.org/Vol-3792/paper25.pdf
|volume=Vol-3792
|authors=Richard Ostertág
|dblpUrl=https://dblp.org/rec/conf/itat/Ostertag24
}}
==Enforcing Fresh Nonces with Affine Type System
==
https://ceur-ws.org/Vol-3792/paper25.pdf
Enforcing fresh nonces with affine type system
Richard Ostertág
Department of Computer Science, Faculty of Mathematics, Physics and Informatics, Comenius University, Bratislava, Slovakia
Abstract
Cryptographic algorithms and protocols often need fresh random numbers as parameters (e.g. nonces). Failure to satisfy this
requirement lead to vulnerable implementation and can result in security breach. We show how affine type systems and static
type checking can be used to enforce the correct generation of a new fresh random number for each function invocation.
Keywords
Secure coding, Nonce, Static checking, Substructural type systems, Rust
1. Introduction algorithm. Alternatively, we can enforce the use
of a specific, vetted software implementation.
The security of various cryptographic constructions re- For this first part, we will employ abstract data
lies on unique or even unpredictable values. Examples types with hidden data constructors, to ensure
include nonces in cryptographic protocols, initializa- that only approved random number generators
tion vectors in modes of symmetric encryption, salts can produce nonce values.
in password-based key derivation functions and others. 2. Preventing Reuse of Random Numbers:
These values are often generated as a random numbers In the second part, we will ensure that once the
of prescribed length. generated random number is used, it cannot be
Programmers who are not experts in cryptography reused for the second time.
might assume that it is not strictly necessary to generate Substructural type systems which enforce single
a new random number every time. Some of them may be (or at most single) use semantics on values, can
lazy and provide fixed numeric constant instead of a new be utilized for this purpose. This approach can be
random number for each use. After all, the cryptographic applied not only to languages that support linear
construction will “correctly”1 work even with this fixed (single use) types but also to any language with
numeric constant. However, if the no-reuse principle is similar features, such as ownership and borrow-
not followed, it can lead to a serious security vulnerability ing in Rust, affine types in Haskell, or uniqueness
in the resulting application (which is not visible at first types in Clean. We will illustrate this concept
glance). A well-known example of this issue is “forbidden using the Rust programming language.
attack” for AES-GCM [1], but e.g. see also [2].
In this paper, we propose a method which demonstrate In Section 2, we describe the key features of abstract
how to implement a cryptographic library that would data types necessary to enforce proper random number
allow the compiler to detect incorrect (i.e. repeated) use generation. Next, in Section 3, we introduce the funda-
of such one-time random numbers at compile time. We mental concepts of substructural type systems, focusing
will divide this task into two main parts: on linear and affine type systems that provide strict con-
trol over resource usage, which we utilize to prevent the
1. Ensuring Proper Random Number Generation: reuse of random numbers. In Section 4, we then explore
In the first part, we ensure that the function ex- the unique features of the Rust programming language,
pecting a random number gets as an argument including traits, ownership, move semantics, and bor-
a random number generated by an “approved” rowing rules, which we leverage to implement the nonce
method. E.g. a true random number generated module. Finally, in Section 5, we demonstrate how to use
by a specialized hardware device and not just the nonce module in a cryptographic library to enforce
some pseudorandom number generated by weak correct nonce usage.
ITAT’24: Workshop on Applied Security, September 20–24, 2024, 2. Abstract data types
Drienica, SK
Envelope-Open richard.ostertag@fmph.uniba.sk (R. Ostertág) Abstract data types (in short ADTs) serve as a fundamen-
Orcid 0000-0002-6560-1515 (R. Ostertág) tal abstraction mechanism in computer science, providing
© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License
CEUR
Workshop
http://ceur-ws.org
ISSN 1613-0073
a formal specification for data types that decouples their
Attribution 4.0 International (CC BY 4.0).
CEUR Workshop Proceedings (CEUR-WS.org)
Depending on the cryptographic construction, it might (for exam- behavior from their concrete implementation. ADTs are
Proceedings
1
ple) still correctly encrypt and decrypt messages. defined by their external behavior, such as operations like
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
insertion and deletion, while concealing the underlying 1 mod nonce {
implementation details from the user. This encapsulation 2 // A public struct with a private
grants implementers the flexibility to employ any inter- 3 // random value of type u128
nal data structures or modify their approach in the future. 4 pub struct Nonce {
As long as the external behavior (interface) remains con- 5 val: u128,
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 different. For example, if a 21 // The Copy and Clone traits are
more efficient data structure becomes available, the inter- 22 // intentionally not implemented
nal implementation of the ADT can be updated without 23
affecting 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 sufficient 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 [3] utilising only
instantiation of structs with private field is prohibited. ADTs. Additionally, it is challenging to enforce rules pre-
In this case for instance it is invalid to write let nonce venting clients from erroneously closing files multiple
= Nonce { val: 42 } . The only way for the client to times or forgetting to close them altogether. Similarly,
create a nonce is to invoke a public constructor method with our Nonce example, there is no static way to stop
like let mut nonce = nonce::Nonce::new() . the client from using one nonce value multiple times just
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.
3. Substructural type systems context
Before presenting our proposed solution using substruc- ⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞
Γ1 , 𝑥 ∶ 𝜏𝑥 , 𝑦 ∶ 𝜏𝑦 , Γ2 ⊢ 𝑒 ∶ 𝜏
(Exchange)
tural type system, it’s essential to provide a brief overview Γ⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟⏟
1 , 𝑦 ∶ 𝜏 𝑦 , 𝑥 ∶ 𝜏𝑥 , Γ2 ⊢ 𝑒 ∶ 𝜏
of what substructural type systems are [3] and how they
permutated context
are implemented within the well-known Rust program-
ming language [4]. The second property, weakening, indicates that adding
Linear and affine 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 affine) 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 en-
Γ, 𝑥2 ∶ 𝜏𝑥 , 𝑥3 ∶ 𝜏𝑥 ⊢ 𝑒 ∶ 𝜏
able us to enforce the one-time use of random numbers, (Contraction)
thereby mitigating potential security vulnerabilities as- Γ, 𝑥1 ∶ 𝜏𝑥 ⊢ [𝑥2 ↦ 𝑥1 , 𝑥3 ↦ 𝑥1 ]𝑒 ∶ 𝜏
sociated with nonce reuse in cryptographic applications. In his book [3], Pierce employs simply-typed lambda
This approach not only leverages Rust’s robust type sys- calculus as a foundation to introduce the concepts of
tem but also showcases the practical application of ad- linear and ordered lambda calculus. While the intricate
vanced type theories in real-world software development. details of these theoretical underpinnings are beyond the
scope of our paper, we encourage interested readers to
3.1. Structural Properties consult Pierce’s work for a comprehensive exploration.
His book provides an in-depth discussion on the princi-
In accordance with Pierce’s work [3] based on simply-
ples of substructural type systems and their applications,
typed lambda calculus, we will treat the type-checking
making it an valuable resource for those looking to delve
context, denoted as Γ, as a straightforward list of variable-
deeper into this topic.
type pairs, 𝑥 ∶ 𝜏𝑥 , where 𝑥 represents a variable and 𝜏𝑥
denotes its type.
The comma operator (,) serves to append a pair to the 3.2. Substructural Type Systems
end of the type-checking context (e.g. Γ1 , 𝑥 ∶ 𝜏𝑥 ), or to A substructural type system is any type system that is
concatenate two type-checking contexts (e.g. Γ1 , Γ2 ). Let designed so that one or more of the structural properties
us denote by Γ ⊢ 𝑒 ∶ 𝜏 that, within the context Γ, we can do not hold [3]. Different substructural type systems
type-check that the term 𝑒 has the type 𝜏. arise when different properties are withheld.
We denote the substitution of the term 𝑦 for the free
variable 𝑥 in the term 𝑒 by [𝑥 ↦ 𝑦]𝑒. We assume that 𝑥 and Linear type systems ensure that every variable is used
𝑦 have the same type, ensuring that the resulting term exactly once by allowing exchange but not weak-
[𝑥 ↦ 𝑦]𝑒 is also correctly typed (in simply-typed lambda ening or contraction.
calculus). Instead of writing [𝑥3 ↦ 𝑥4 ]([𝑥1 ↦ 𝑥2 ]𝑒), we
use the more concise form [𝑥1 ↦ 𝑥2 , 𝑥3 ↦ 𝑥4 ]𝑒. Affine type systems ensure that every variable is used
at most once by allowing exchange and weaken-
premise ing, but not contraction.
(Typing rule)
conclusion
Relevant type systems ensure that every variable is
Finally, by typing rule we mean that if its premise is
used at least once by allowing exchange and con-
true, then we can conclude that its conclusion also holds.
traction, but not weakening.
Lets discuss three basic structural properties. The first
property, exchange, indicates that the order in which Ordered type systems ensure that every variable is
we write down variables in the context is irrelevant. A used exactly once and in the order in which it is
corollary of exchange is that if we can type check a term introduced. Ordered type systems do not allow
with the context Γ, then we can type check that term any of the structural properties.
with any permutation of the variables in Γ.
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 du-
diagram, 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 nec-
essary, 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).
affine (E,W) relevant (E,C)
4.2. Ownership rules
+W +C In Rust, when a value is assigned to a variable, the vari-
able becomes the “owner” of that value. When the owner
linear (E)
variable goes out of scope, the value is automatically deal-
located. Rust enforces that there can only be one owner
+E
for a value at a time. This is the essence of substructural
ordered (none) type system in Rust [6]:
Figure 1: Relationship between linear and other substructural • Each value has a variable that is called its owner.
type systems. • There can be only one owner at a time.
• When the owner goes out of scope, the value will
be dropped (memory will be deallocated).
All type systems below unrestricted (aka. structural)
are called substructural type systems. It might be pos-
sible to define type systems containing other combina- 4.3. Move semantics
tions of structural properties, such as contraction only Move semantics in Rust is a fundamental concept that
or weakening only, but so far researchers have not found allows the transfer of ownership of a value from one
applications for such combinations [3]. Consequently, variable to another. When a value is assigned from one
they are excluded from the diagram. 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 [7]. In other words, variable
Ownership is Rust’s most unique feature which is closely bindings have “move semantics” if their type does not
related to the concept of substructural type systems in implement the Copy trait; otherwise, they have “copy
that both systems enforce strict rules about how data is semantics”.
accessed and modified to ensure safety and correctness. After a move, the original variable is no longer valid
It enables Rust to make memory safety guarantees with- and cannot be used. Move semantics can improve per-
out needing a garbage collector. In Rust, the memory is formance by avoiding deep copies of data. Instead of
managed through a system of ownership with a set of copying the data, Rust only copies the pointer to the data
rules, that the compiler checks at compile time. None of and invalidates the original pointer. Single owner allows
the ownership features slow down the program while it for values to be deallocated as soon as their owner goes
is running (unlike garbage collection). out of the scope.
4.1. Rust traits 4.4. Borrowing rules
Traits in Rust serve as a way to define shared behavior. If you need to access or modify a value without transfer-
They are similar to interfaces in other programming lan- ring ownership, you can borrow a reference to it. There
guages. They allow to specify methods that types must are two types of borrowing in Rust:
implement, enabling polymorphism and code reuse. For
more see e.g. [5]. • Immutable borrowing:
You can have multiple immutable references to a
2
value, but you cannot modify the value through
Fig. 1 is based on similiar image in [3].
these references. This prevents data races be-
stack heap
cause multiple threads can read a value without
the risk of it being modified simultaneously.
• Mutable borrowing: s1
You can have only one mutable reference to a ptr
value, and no other references (mutable or im-
mutable) can coexist with it. This enforces exclu- len 5 index value
sive access to the value, ensuring that only one capacity 5 0 h
part of the code can modify it at a time. 1 e
2 l
s2
1 fn borrowing() { ptr 3 l
2 let s1 = String::from("Hello"); 4 o
len 5
3 // ^^ move occurs because `String` does
capacity 5
4 // not implement the `Copy` trait
5
6 let s2 = s1; // value moved from s1 to s2
7
Figure 2: Memory representation of variables s1 and s2
8 println!("{}, world!", s1);
9 //error: val. borrowed ^^ here after move
10 } On Listing 3 we implement function need_new_
random_u128_every_time to demonstrate function sig-
nature 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 right . 73
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. [6].
Listing 3: Example of function with nonce as argument
5. The solution
When function need_new_random_u128_every_time
The solution in Rust is syntactically very simple because
is called, then value ownership is moved from the local
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 implement-
ing Copy trait in Nonce type. 6. Conclusion
We have demonstrated how to use abstract data types and
3
Fig. 2 is based on similiar image in [6]. substructural type systems for enforcing the freshness of
1 fn main() { ch10-02-traits.html, with contributions from the Rust
2 // Structs with private fields can be Community.
3 // created only using public constructors [6] S. Klabnik, C. Nichols, What is ownership?, 2024.
4 let mut nonce = nonce::Nonce::new(); URL: https://doc.rust-lang.org/book/ch04-01-what-
5 need_new_random_u128_every_time(nonce); is-ownership.html, with contributions from the Rust
6
Community.
7 nonce = nonce::Nonce::new(); [7] S. Klabnik, C. Nichols, Trait std::marker::Copy,
8 need_new_random_u128_every_time(nonce); 2024. URL: https://doc.rust-lang.org/std/marker/trait.
9
Copy.html, with contributions from the Rust Com-
10 need_new_random_u128_every_time( munity.
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 affine 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.
Acknowledgments
This publication is the result of support under the
Operational Program Integrated Infrastructure for the
project: Advancing University Capacity and Compe-
tence in Research, Development a Innovation (ACCORD,
ITMS2014+:313021X329), co-financed by the European
Regional Development Fund.
References
[1] H. Böck, A. Zauner, S. Devlin, J. Somorovsky,
P. Jovanovic, Nonce-Disrespecting adversaries:
Practical forgery attacks on GCM in TLS, in:
10th USENIX Workshop on Offensive Technologies
(WOOT 16), USENIX Association, Austin, TX, 2016.
URL: https://www.usenix.org/conference/woot16/
workshop-program/presentation/bock.
[2] A. Joux, Authentication failures in NIST version of
GCM, 2006. URL: https://csrc.nist.gov/csrc/media/
projects/block-cipher-techniques/documents/bcm/
joux_comments.pdf.
[3] B. C. Pierce (Ed.), Advanced topics in types and pro-
gramming languages, The MIT Press, MIT Press,
London, England, 2004.
[4] S. Klabnik, C. Nichols, The Rust programming lan-
guage, No Starch Press, San Francisco, CA, 2019.
[5] S. Klabnik, C. Nichols, Traits: Defining shared be-
havior, 2024. URL: https://doc.rust-lang.org/book/