# Static Information Flow Control Made Simpler

Hemant Gouni<EMAIL_ADDRESS>University of MinnesotaMinneapolisMinnesotaUSA
and  Jonathan Aldrich<EMAIL_ADDRESS>Carnegie Mellon
UniversityPittsburghPennsylvaniaUSA

###### Abstract.

Static information flow control (IFC) systems provide the ability to restrict
data flows within a program, enabling vulnerable functionality or confidential
data to be statically isolated from unsecured data or program logic. Despite
the wide applicability of IFC as a mechanism for guaranteeing confidentiality
and integrity— the fundamental properties on which computer security relies—
existing IFC systems have seen little use, requiring users to reason about
complicated mechanisms such as lattices of security labels and dual notions of
confidentiality and integrity within these lattices. We propose a system that
diverges significantly from previous work on information flow control, opting
to reason directly about the data that programmers already work with. In doing
so, we naturally and seamlessly combine the clasically separate notions of
confidentiality and integrity into one unified framework, further simplifying
reasoning. We motivate and showcase our work through two case studies on TLS
private key management: one for Rocket, a popular Rust web framework, and
another for Conduit, a server implementation for the Matrix messaging service
written in Rust.

Information Flow Control, Security Type Systems, Accessible Correctness

††copyright: none††booktitle: HATRA ’22: Human Aspects of Types and Reasoning
Assistants, December 5, 2021, Auckland, New Zealand††ccs: Software and its
engineering Formal software verification††ccs: Software and its engineering
Specification languages

##  1\. Introduction

Security is a paramount concern in a pervasively digital world. The vast
increase in digitization of the past decade has come with a proportional
increase in the severity of data breaches (Warren et al., 2016), warranting
renewed research into accessible, yet powerful, methods of declaring and
enforcing security specifications. Information flow control is a program
analysis technique that aims to prevent undesirable data flows. For example,
in a program implementing a simple web application for performing
authentication, there may be modules for (1) performing network I/O, (2)
validating user input, (3) checking passwords, and (4) interacting with a
database. A reasonable information flow specification, shown in Fig. 1, might
be that (1) should never flow to (3) or (4), and that data from (4) should
never flow to (1). Green (solid) arrows in the diagram denote the flows
required for the program to function, and red (dashed) arrows denote the flows
which must be prevented to ensure the program’s security. A flow from, for
instance, (1) to (4), occurs when data from (1), or which is transitively
dependent on (1), flows to (4). Note that certain flows in the diagram, such
as from (1) to (4), are denied directly but permitted transitively—
specifically, after data from (1) passes through (2). This is addressed during
the case study in Section 2.

Figure 1. Permitted flows in our example program

A classical information flow control system (Myers, 1999; Simonet, 2003) might
support the specification of the flow architecture in Fig. 1 by providing two
lattices: one for reasoning about confidentiality, or the property that
confidential data does not leak to inappropriately visible places, and one for
integrity, or the property that untrusted data does not propagate to
inappropriately integral places. All data in the program must have a label
relevant to each lattice, denoting its levels of confidentiality and
integrity. Two separate lattices are required for each property owing to the
duality between them: two distinct and opposing invariants must be enforced
when data is labeled as both highly confidential and highly integral, such as
with db_handle in Fig. 1. First, it must never flow to data labeled as being
of low confidentiality, such as network_io. Second, data labeled as being of
low integrity, again like network_io, must never flow to db_handle. This
separate treatment complicates reasoning— for example, Jif (Pullicino, 2014),
a state of the art IFC system for Java, provides entirely new (dual) semantics
for lattice operations when reasoning about integrity versus confidentiality.

Our system resolves this issue by presenting a single, straightforward
abstraction for declaring information flow policies, simplifying
specifications while retaining expressivity. Instead of organizing data inside
a lattice and reasoning about flows in the context of it, we opt to allow
programmers to directly specify which flows between places in a program are
not permitted, as presented in the architecture in Fig. 1. A declaration flow
b ->! c states that data affected by variable b cannot flow to variable c, and
a declaration flow mod network_io ->! mod db_handle states that data affected
by the network_io module cannot flow to the db_handle module. We will refer to
the part before the arrow as the source, and the part after as the
destination. This streamlined annotation language contributes to a system
which is:

  1. (1)

Uniform: a flow annotation flow b ->! c may be an integrity specification, a
confidentiality specification, or potentially both— the programmer need not
shift their reasoning

  2. (2)

Incremental: our approach to flow annotations encourages partial and local
specifications on the way to proving higher level program properties, and

  3. (3)

Simple: we provide a small number of straightforward constructs which are
highly general and composable, minimizing changes needed to the semantics of
the language and easing adoption of the system by new users.

We will explore these properties further by analyzing cryptographic key
management in two popular Rust programs, Rocket and Conduit. A brief formal
description of our IFC system, as an extension to the Rust type system, is
provided in the appendix for the curious reader.

##  2\. Motivation: Managing Keys

###  2.1. Case Study: Rocket

1flow self.config.tls.key ->! fn io!();2flow self.config.tls.key ->!
*;34...56let mut listener: Either<TcpListener, TlsListener> =7
Left(TcpListener::bind(addr).await.map_err(ErrorKind::Bind)?);89if
self.config.tls_enabled() {10 if let Some(ref config) = self.config.tls11 with
flow self.config.tls.key -> config {1213 let conf =
config.to_native_config().map_err(ErrorKind::Io)?14 with flow
self.config.tls.key -> conf;1516 flow self.config.tls.key -> listener;1718
listener =19 Right(TlsListener::bind(addr,
conf).await.map_err(ErrorKind::Bind)?);20 }21}2223listener = allow
listener;2425...

Figure 2. Verifying non-leakage of TLS key data in Rocket

Rocket is a fully fledged and widely used HTTP framework for Rust. Like many
web frameworks, it provides optional support for serving traffic over
Transport Layer Security, or TLS, connections. TLS is an essential feature for
securing data between clients, such as browsers, and servers, encrypting data
in transit. A critical component of TLS is a public-private keypair held by
the server, in this case Rocket. Each domain which aims to communicate
securely with web browsers and clients at large must obtain a certified
keypair, which is valid for any traffic served by it. While a typical web
service consists of a large number of physical servers, each of them may use
the same TLS keypair, assuming they are serving a single domain. This is
convenient, but risky— leakage of the private key for a domain from any of its
servers risks compromising the security of the entire service. It is
essential, then, that this does not occur, and an IFC system may be able to
provide that assurance.

Most of our discussion will be directed at the particular Rocket code path
that deals with conditionally configuring TLS functionality, shown in Fig. 2.
Specifically, we analyze the function default_tcp_http_server in file
core/lib/src/server.rs, on commit 2fc4b156 of the Rocket git repository. In
order to render this section of code amenable to information flow
verification, some minimal refactoring was required; we will return to this
later. We focus our attention here because it is the primary part of the
codebase where key data is accessed directly (through to_native_config and
TlsListener::bind on lines 13 and 19), increasing the potential for leaks and
need for verification. Verification of the latter two functions is not as
interesting, because their implementation is largely straightforward or
reliant on primitives provided by Rustls, a TLS library for Rust. A summary of
the displayed Rocket code follows.

Ignoring the information flow constructs, the code in Fig. 2:

  * •

On lines 6 and 7: Binds a variable, listener, which initially holds a TCP
socket

  * •

On lines 9 and 10: Checks that TLS is enabled and that a TLS configuration is
provided

  * •

In lines 13 through 19: Extracts the provided TLS configuration into a
structure understood by TlsListener::bind and calls it, setting listener to
the returned TLS socket.

We now discuss the IFC specifications for self.config.tls.key, which contains
key data, in Fig. 2. The flow declaration on the first line prohibits the
private key from flowing transitively to any functions which could perform I/O
operations, such as those in std::io, std::fs, std::net, std::ffi, and
std::os. The same property could be expressed as a series of individual flow
declarations on each relevant namespace, but the use of a macro here provides
a convenient abstraction. The next declaration employs a special place
understood by flow rules: *, which applies to all variables, along with the
return value. This ensures that key data does not leak to any place without
being explicitly permitted to do so. We care about flows to places, instead of
merely flows to I/O operations, because of abstraction: a module may never
perform I/O internally, but it may communicate with another that does, and
verifying that it does so safely requires assertions about information flow
inside the module. Permission for flows may be granted in two ways: through
overriding the flow rules we have already declared, or by using the allow
construct.

Overriding occurs whenever a rule is declared that is more specific than
another. Specificity is determined by the length of the prefix being accessed
within a variable or namespace. For example, given a rule flow b ->! c in some
scope, where b is a struct with field f, a rule flow b.f -> c declared in that
scope would act as an override, permitting flows from b.f to c (but not from
any other fields of b). Additionally, there are two invariants enforced by the
system on flow declarations, which ensure that it can always find a maximally
specific rule for any given flow. First, it is an error to declare
contradictory flow rules. Second, in the case of two opposing flow rules where
one flow rule has a more specific destination than another, and the other a
more specific source, the one that denies the flow is chosen. This might occur
in the case of two flow rules flow a.b ->! c and flow a -> c.d— a flow from
a.b to c.d would be denied because the first rule is denies the flow. This is
done for safety: denied flows are visible, but permitted flows are not. We can
now analyze the last three flow rules in Fig. 2.

Starting with the rule on line 11, we see slightly different syntax, with
flow, in the declaration. This is done because we cannot declare the flow rule
on config before it has been bound, and by the time the binding happens, it is
already too late, and a violation of the rule on line 2 is inevitable. with
flow is syntactic sugar provided for the let construct which inserts a flow
declaration between binding and initialization. We proceed similarly for the
flow rules on lines 14 and 16, overriding the flow rule on line 2 as needed,
but another element bears discussion: function calls. When a function is
called with data affected by rules denying flows, the information flow control
system checks that the flow policies declared by the function are compatible
with those from the calling context. Only mutably referenced arguments, the
return value, and any restrictions on flows to functions are checked here; the
precise mechanics are discussed further in Appendix A.1. Importantly, we only
look at the publicly visible portion of a function’s signature, preserving
abstraction and ensuring modularity. We are able to treat functions in this
way because Rust programs generally do not make use of global mutable state—
treating it as an error, then, does not result in a materially more
conservative system. As a result, for functions which do not perform IO, we
must only consider their arguments and return value. In this case, the call to
to_native_config receives an immutable reference and does not take any other
arguments, so the with flow declaration suffices to allow the call. The
function call on line 19, which takes its two arguments by move, passes
similarly. Note that, having explicitly permitted flows from
self.config.tls.key to config, conf, and listener, flows from these four
variables to any other variables will now cause an error.

Lastly, we arrive at the assignment to listener on the second-to-last line.
allow evaluates an expression and returns the result, but without any of the
expression’s dependencies. It is comparable to other information flow systems’
declassify (for confidentiality) and endorse (for integrity) constructs (Hedin
and Sabelfeld, 2012) in providing an explicit escape hatch, but generalizes
over both. In this case, we use allow to remove listener’s dependency on
self.config.tls.key, assigning it to itself so that further uses will not
produce errors. The usage of allow here is safe because, importantly,
TlsListener no longer provides access to raw key data, only to signing
operations with the key. This is still a concern, but a much lesser one— data
dependencies on listener do not risk revealing information about the
cryptographic key. Further, it is reasonable to wonder why we must use allow
on listener, outside the scope of the preceding conditionals, instead of on,
say, conf in the argument list to TlsListener::bind. Control flow dependencies
are what make this necessary. These are implicit flows that take place when
explicit flows occur inside a conditional branch. In Fig. 2, this crucially
happens when listener is assigned to the result of evaluating
TlsListener::bind, where it gains a dependency on self.config.tls.key not only
because of the function’s return value, but also because the guards for both
if statements, on lines 9 and 10, are dependent on self.config.tls.key. As a
result, applying allow inside the conditional would remove the dependency from
bind’s return value, but not from the conditional branches, which would
require two additional usages on the guards themselves. Instead, we do so once
outside both conditionals and reassign to listener.

Control flow dependencies also explain why a minor refactor was necessary in
order to ease information flow reasoning. default_tcp_http_server, as present
in the Rocket repository at the referenced commit, unnecessarily includes
several assignments inside the conditionals, in addition to logic afterwards
which depends on those assignments. Moving all of this functionality outside
of the conditional branches removes unneeded dependencies on the value of
self.config.tls.key and additionally results in less overall code duplication.
In general, we believe that the introduction of an information flow control
type system to programs which did not have it before will encourage shifts in
coding style, just as typed programs differ from untyped programs in order to
better cooperate with (and take better advantage of) the type system.

To summarize, we show that, under our formal system, we can concisely prove a
strong information flow property about TLS key management within Rocket,
specifically, that no TLS key data leaks from default_tcp_http_server. Though
bugs were not identified while demonstrating our theory of information flow,
note that our specifications would suffice to prevent the occurrence of future
bugs within relatively complicated and error-prone code. Moreover, this
property is local, only concerning the function itself and two of its callees.
Specifications beyond those discussed here could be used to prove higher level
properties about the absence of key leakage from the entirety of Rocket. We
now apply the mechanisms we have discussed here to a second program.

###  2.2. Case Study: Conduit

Conduit is a Rust implementation of the server portion of the Matrix chat
protocol. As a federated messaging service (meaning there does not exist a
single canonical server, but a cooperating network of them, much like email),
Matrix relies heavily on cryptography to secure and authenticate message
contents. This includes communication between Matrix servers themselves. We
analyze a similar situation to the one identified with Rocket, in which
complicated application initialization logic executes within a context that
contains raw key data, and so might benefit from the use of IFC to explicitly
enforce security policies. We specifically analyze the load function in file
src/database/globals.rs, on commit 566dc0a of the Conduit git repository. The
relevant snippet of code is shown in Fig. 3. As before, we begin with a brief
summary of its functionality.

1...23flow keypair_bytes ->! fn io!();4flow keypair_bytes ->! *;56let mut
parts = keypair_bytes.splitn(2, |&b| b == 0xff)7 with flow keypair_bytes ->
parts;89let keypair =
utils::string_from_bytes(...).map_err(...).and_then(...)10
.and_then(|(version, key)| {11 ruma::signatures::Ed25519KeyPair::from_der(key,
version)12 .map_err(|_|13 Error::bad_database("Private or public keys are
invalid."))14 })15 with flow keypair_bytes -> keypair;1617let keypair = allow
keypair;1819...

Figure 3. Verifying that Conduit does not leak Matrix server keys

  * •

Lines 6 and 7: Process the raw bytes representing the key into a version
indicator and a key

  * •

Line 9: Perform several steps of validation on the version string and key data

  * •

Lines 10 through 15: Pass the validated data to a library function that
handles cryptography for Matrix applications

Addressing the information flow constructs in Fig. 3, we start with the same
two declarations as for Rocket. The first, on line 3, prohibits flows to I/O
functions, which might allow sensitive information to escape, and the second
prohibits flows to any variables, along with the return value of the current
function. We allow the flow on line 7 using the with flow construct and our
notion of overriding flow policies. Overriding occurs here because parts is
more specific than *. Note, again, that flows from parts will still cause
errors.

A similar with flow declaration is made on line 15, again using overriding.
However, lines 10 through 12, immediately prior to it, warrant further
discussion due to their use of closures. The treatment of closures— and higher
order functions in general— is straightforward in our system. Besides the
checks done for function calls, discussed in Section 2.1, we must perform two
additional checks involving any data captured by the closure. First, the
captured data is added to the set of dependencies which will flow through the
closure’s return value, or to any mutable references passed as arguments to
it. Second, we ensure that the closure is never passed any information that
might inappropriately flow to variables captured by it. The flow policy for
the current scope remains active for the body of the closure itself, so any
potential flows between captured variables will be caught when the closure is
declared. Luckily, however, the usages on line 10 and 12 do not need these
considerations. The closure declaration on line 10 does not close over
anything, only taking two arguments, neither of which is a mutable reference,
and returning key data, wrapped in a Result type. The closure on line 12 is
similar, taking one argument (which contains an error value, if applicable)
and returning another Result to keypair. Accordingly, the with flow
declaration on line 15 suffices to allow keypair_bytes to flow to keypair.

The function call on line 11 securely abstracts away raw key data, rendering
it inaccessible, just as was the case with Rocket. It is again safe, then, to
use allow on keypair, assigning it to itself to prevent further information
flow violations from uses of it. Having analyzed this snippet from the Conduit
codebase, we note that it is highly similar to the Rocket code before it, both
in terms of the information flow control issues raised and the simple,
declarative solutions offered by our system. We expect this general pattern of
information flow control to arise consistently when managing sensitive data
within application configuration and setup logic.

We introduce one final information flow pattern that arises in the Conduit
codebase as a consequence of the pervasive use of cryptographic operations in
the Matrix protocol, and discuss a natural method of addressing it offered by
our system. This time, the data in question does not grant direct access to
the private key, only to cryptographic operations with it. It does, however,
exist alongside application logic that interacts with user input over the
network, so IFC is once again warranted. Fig. 4 shows part of the
implementation of create_invite_route in file src/server_server.rs on the same
commit. We start, as usual, with a short summary of the code.

1...23flow db.globals.keypair() ->! fn io!();4flow db.globals.keypair() ->!
*;56...78let mut signed_event = utils::to_canonical_object(&body.event)9
.map_err(|_| Error::BadRequest(ErrorKind::InvalidParam,10 "Invite event is
invalid."))?;1112ruma::signatures::hash_and_sign_event(db.globals.server_name().as_str(),13
allow db.globals.keypair(), &mut signed_event, &body.room_version)14
.map_err(|_| Error::BadRequest(ErrorKind::InvalidParam,15 "Failed to sign
event."))?;1617...

Figure 4. The event signing pattern in Conduit

  * •

Lines 8 through 10: Create a JSON object with a reproducible serialized
representation to prepare it to be hashed, assigning it to signed_event

  * •

Lines 12 through 15: Hash and sign the JSON object by passing it,
db.globals.keypair(), and a mutable reference to signed_event to a library
function responsible for handling cryptography; signed_event is assigned the
result through the reference

Preceding and following the code in Fig. 4 is a large amount of logic for
inviting a user to a room through the Matrix protocol— create_invite_route
implements the relevant API endpoint for doing so. This pattern arises not
just in this function, but throughout Conduit, for every API endpoint which
must use key data. In other words, large portions of Conduit both have access
to db.globals.keypair(), which is passed to every function that needs it, and
process networked user input. Our IFC system adapts naturally to this
challenge because of its focus on local reasoning.

We begin with the usual flow declarations on lines 3 and 4, restricting
db.globals.keypair() from flowing to any functions which perform I/O, any
variables, or the return value. It should be noted that while
db.globals.keypair() cannot reveal raw key data, it may still produce
sensitive information (such as signed events), so data dependent on it should
be prevented from flowing to I/O. We use a single allow in the call to
ruma::signatures::hash_and_sign_event on line 12, because signed_event does
not pose any risk of compromising access to the key.

Though this is an exceptionally simple flow specification, note that we have
also verified an exceptionally strong information flow property. Besides
signed_event, no other data in the program is permitted to invoke, or use data
from invoking, db.globals.keypair(). Program logic not pictured in Figs. 3 and
4 for brevity requires further specifications in order to pass information
flow checking (in particular, functions to which db is passed, whose flow
policies would need to be updated in order for the call to succeed), but the
added complexity is negligible.

###  2.3. What about lattices?

We now briefly compare our system to one implementing a generic lattice-based
theory of information flow. We avoid complicated constructs such as principals
(Myers and Liskov, 2000) and robust declassification (Myers et al., 2004) for
which we currently lack meaningful comparisons.

The most apparent advantage of our system, relative to any that employs
lattices, is that our specifications act as a declarative description of the
desired information flow policies in effect for any program scope. At a
glance, it is trivially easy to determine the desired flow architecture, what
data is critical, and how to work within programs annotated with IFC
specifications. Should the user desire to enforce, taking Fig. 2 for example,
that self.config.tls.key does not leak to unsecured areas in the program, it’s
necessary only to declare precisely that property, explicitly permitting flows
where needed and explicitly disengaging the IFC system once the language’s
normal abstraction mechanisms have guaranteed the property at hand. A lattice-
based system would need to talk about the property that the key does not leak
indirectly, giving it a label that indicates high confidentiality and
providing other data with labels of lower confidentiality. Adding additional
flow restrictions, especially integrity policies, would make the desired
information flow architecture much less clear in this setting.

Finally, a last point should be noted about label-based reasoning versus the
direct usage of program places: locality. Generally, our system’s ability to
reason about programs locally is not due to any increase in formal reasoning
power over prior work, but can instead be owed to its removal of labels as a
mechanism for abstracting over places in a program— labels naturally encourage
the creation of specifications that attempt to talk about multiple,
potentially disparate, places at once, instead of incrementally declaring flow
policies on critical data and proving them. For instance, when using a system
such as Flow Caml (Simonet, 2003), a lattice of security levels is declared
globally and enforced for the whole program at once.

##  3\. Conclusion and Related Work

Much related work on information flow control, particularly usable information
flow control, includes support for dynamic verification when static reasoning
presents too high a barrier— (Myers, 1999) does just this. The formal system
described here, however, carries enough novelty in the fully static realm to
warrant an exclusive focus; future work may introduce dynamic elements.
(Simonet, 2003) increases the usability of its IFC system by precisely
inferring security labels, which may similarly be an interesting direction for
future work. (Crichton et al., 2022) provides a modular information flow
analysis for Rust programs on which we build our formalism, but it does not
provide a way to specify intended restrictions on information flow.

We have reviewed classical systems of information flow, introducing a
simplified specification language and system constructed around it which we
hope will aid in advancing the accessibility of information flow. We conducted
two case studies in which we demonstrated the natural applicability of our
system to local reasoning. After proving the soundness of our system, we hope
to pursue a practical implementation for use on real-world Rust programs.

###### Acknowledgements.

This research was sponsored by Department of Defense award H9823018D0008 and
National Science Foundation award CCF-1901033. Any opinions, findings, and
conclusions or recommendations expressed in this material are those of the
author and do not necessarily reflect the views of the Department of Defense
or the National Science Foundation.

## References

  * (1)
  * Crichton et al. (2022) 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_ (San Diego, CA, USA) _(PLDI 2022)_. Association for Computing Machinery, New York, NY, USA, 1–14.  https://doi.org/10.1145/3519939.3523445
  * Hedin and Sabelfeld (2012) Daniel Hedin and Andrei Sabelfeld. 2012.  A perspective on information-flow control.  In _Software safety and security_. IOS Press, 319–347.
  * Myers (1999) 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_ (San Antonio, Texas, USA) _(POPL ’99)_. Association for Computing Machinery, New York, NY, USA, 228–241.  https://doi.org/10.1145/292540.292561
  * Myers and Liskov (2000) Andrew C Myers and Barbara Liskov. 2000.  Protecting privacy using the decentralized label model.  _ACM Transactions on Software Engineering and Methodology (TOSEM)_ 9, 4 (2000), 410–442.
  * Myers et al. (2004) Andrew C Myers, Andrei Sabelfeld, and Steve Zdancewic. 2004\.  Enforcing robust declassification. In _Proceedings. 17th IEEE Computer Security Foundations Workshop, 2004._ IEEE, 172–186.
  * Pullicino (2014) Kyle Pullicino. 2014\.  Jif: Language-based Information-flow Security in Java.  _CoRR_ abs/1412.8639 (2014).  arXiv:1412.8639 http://arxiv.org/abs/1412.8639
  * Simonet (2003) Vincent Simonet. 2003\.  The flow caml system.  _Software release. Located at http://cristal. inria. fr/~ simonet/soft/flowcaml_ 116 (2003), 119–156.
  * Warren et al. (2016) Tucker Warren, Jared Favole, Scott Haber, and Emily Hamilton. 2016.  Cybercrime costs more than you think.  _Hamilton Place Strategies Report_ (2016).
  * Weiss et al. (2019) Aaron Weiss, Daniel Patterson, Nicholas D. Matsakis, and Amal Ahmed. 2019.  Oxide: The Essence of Rust.  _CoRR_ abs/1903.00982 (2019).  arXiv:1903.00982 http://arxiv.org/abs/1903.00982

##  Appendix A Appendix

###  A.1. Formal System: Extending Rust

We now formally describe our IFC system as an extension to Rust’s type system.
The formal model of Rust is provided by Oxide (Weiss et al., 2019). We take
inspiration from the work on tracking information flow in Rust presented by
Flowistry (Crichton et al., 2022), though we diverge significantly from it in
order to capture the full expressivity of our system. Rust was chosen as the
foundation for our system because, as noted in (Crichton et al., 2022), the
language already performs a highly precise pointer analysis as part of borrow
checking, which is essential for any information flow system. Users need not
contend with an overly conservative pointer analysis, or with any additional
restrictions imposed by a precise one. Additionally, there is very little
existing work on IFC in Rust, and given the language’s history of embracing
lightweight correctness techniques, we feel that our approach is likelier to
succeed within it. Our extensions to Oxide are colored in brown. We only
consider flows between variables here, because more complicated flow
declarations such as those between functions and modules do not present
additional challenges to the formal system, behaving similarly to the
constructs already handled by it.

$\begin{matrix}\text{Variables}~{}x&\text{Naturals}~{}m,n,k&\text{Concrete
Regions}~{}r&\text{Type Vars.}~{}\alpha\end{matrix}$
$\displaystyle\text{Path}~{}q~{}$ $\displaystyle::=~{}\epsilon~{}|~{}n.q$
$\displaystyle\text{Places}~{}\pi~{}$ $\displaystyle::=~{}x.q$
$\displaystyle\text{Place Exprs.}~{}p~{}$
$\displaystyle::=~{}x~{}|*p~{}|~{}p.n$
$\displaystyle{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\text{Dependency
Exprs.}~{}d~{}}$
$\displaystyle::=~{}{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\delta~{}|~{}p}$
$\displaystyle{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\text{Access
Exprs.}~{}a~{}}$
$\displaystyle::=~{}{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}*~{}|~{}p}$
$\displaystyle\text{Place Expr. Contexts}~{}p^{\Box}~{}$
$\displaystyle::=~{}\Box~{}|~{}*p^{\Box}~{}|~{}p^{\Box}.n$
$\displaystyle\text{Loans}~{}l~{}$ $\displaystyle::=~{}^{\omega}p$
$\displaystyle\text{Ownership Qualifiers}~{}\omega~{}$
$\displaystyle::=~{}\texttt{shrd}~{}|~{}\texttt{uniq}$
$\displaystyle\text{Constants}~{}c~{}$
$\displaystyle::=~{}()~{}|~{}n~{}|~{}\texttt{true}~{}|~{}\ldots$
$\displaystyle\text{Expressions}~{}e~{}$
$\displaystyle::=~{}c~{}|~{}p~{}|~{}\&r\omega p~{}|~{}\ldots$
$\displaystyle\text{Base Types}~{}\tau^{\text{B}}~{}$
$\displaystyle::=~{}\texttt{u32}~{}|~{}\texttt{bool}~{}|~{}\ldots$
$\displaystyle\text{Sized Types}~{}\tau^{\mathrm{SI}}~{}$
$\displaystyle::=~{}\tau^{\text{B}}~{}|~{}\alpha~{}|~{}\ldots$

Figure 5. Oxide’s syntax, extended

Beginning with the syntax, we present the parts of Oxide’s syntax most
relevant to our discussion. We make two additions, the first of which
introduces dependency expressions $d$, combining $\delta$, which tracks
dependencies, and place expressions $p$, which are used by Oxide to represent
values which can be assigned to. The other addition is similar, creating
access expressions $a$, combining *, which appears in Fig. 2, with place
expressions.

Our typing judgement is
$\Sigma;\Delta;\Gamma;\Theta;{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\Pi;\Psi;\Xi}\vdash{}e:\tau{}{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}~{}\bullet~{}\delta}\Rightarrow{}\Gamma^{\prime}{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25};\Pi^{\prime}}$,
which reads “given the global environment $\Sigma$, the type environment
$\Delta$, the stack typing environment $\Gamma$, the continuation typing
environment $\Theta$, the dependency environment $\Pi$, the flow policy
environment $\Psi$, and the branch dependency environment $\Xi$, the
expression $e$ with type $\tau$ and dependencies $\delta$ produces an updated
stack typing environment $\Gamma^{\prime}$ and dependency environment
$\Pi^{\prime}$”. This is similar to the one used by Flowistry, with additional
environments for tracking flow policies and control flow dependencies— the
latter with increased precision.

T-True T-Move
0[] Σ; Δ; Γ; Θ; Π; Ψ; Ξ ⊢ true: bool ∙ ∅ ⇒ Γ; Π Δ; Γ; Θ ⊢uniqπ ⇒ { uniqπ }
Γ(π) = τSInoncopyableΣτSIδ = δ-place(π: τSI, Π) 1[] Σ; Δ; Γ; Θ; Π; Ψ; Ξ ⊢ π:
τ^SI  ∙ δ ⇒ Γ[π ↦ τ^SI^†]; Π
Δ; Γ; Θ ⊢shrdp ⇒ { ¯l} Δ; Γ ⊢shrdp: τSIcopyableΣτSIδ = ⨆∅τSIωp’ ∈ {
¯l}δ-place(p’: τSI, Π) 1[T-Copy] Σ; Δ; Γ; Θ; Π; Ψ; Ξ ⊢ p: τ^SI  ∙ δ ⇒ Γ; Π
∀ i ∈ { 1, …, n } . Σ; Δ; Γi-1; Θ, τ1SI, …, τi-1SI; Πi-1; Ψ; Ξ ⊢ ei: τiSI∙ δi⇒
Γi; Πi∀ i ∈ { 1, …, n } . ∀ p□[δi] ∈ leaves(δi: τiSI) . p□[δ.i] = p□[δi]
1[T-Tuple] Σ; Δ; Γ_0; Θ; Π_0; Ψ; Ξ ⊢ (e_1, …, e_n): (τ_1^SI, …, τ_n^SI)  ∙ δ ⇒
Γ_n; Π_n

Figure 6. A collection of basic typing rules

####  A.1.1. Tracking flows

Our first rule, for the value true, appears in Fig. 6. Bare values are
effectively ignored by the information flow system, producing an empty
dependency expression $\delta$, because flow rules cannot be declared on them.
The next two rules, T-Move and T-Copy, are more interesting, but require the
introduction of a few metafunctions. Much of the theory presented here is
founded on the treatment of places, $p$, as nothing more than the composition
of their leaves. That is, given a place which represents a struct with fields
$f$ and $g$, where $g$ is itself a struct with field $h$, the leaves of $p$
are $f$ and $h$. Dependencies are always leaves— dependency sets contain the
leaves of a place that is depended on, rather than the ‘top level’ place. The
$\operatorname{\delta\text{-}place}{}\\!$ and
$\delta_{1}\prescript{\\{~{}\\!\overline{p}\\!\\!~{}\\}}{\tau^{\mathrm{SI}}}{\sqcup}~{}\delta_{2}$
operations used by T-Move and T-Copy depend on this notion of analyzing a
place expression for the set of atomic places it contains; doing so allows the
analysis to be maximally precise without sacrificing simplicity. We exclude
type constructors, supported through the special inclusion of the Either type
by Oxide, because their treatment is similar to that for fields. Oxide also
does not support the declaration of recursive types, but these can soundly be
treated as leaves themselves in a practical implementation. The definition of
these two metafunctions is shown on the first two lines of Fig. 7.

$\operatorname{\delta\text{-}place}(p:\tau^{\mathrm{SI}},\Pi)=\forall
p_{\mathrm{leaf}}^{\Box}[p]\in\operatorname{leaves}(p:\tau^{\mathrm{SI}})~{}.~{}p_{\mathrm{leaf}}^{\Box}[\delta]=\\{~{}p_{\mathrm{leaf}}^{\Box}[p]~{}\\}\cup\Pi(p_{\mathrm{leaf}}^{\Box}[p]);\delta$
$\delta_{1}\prescript{\\{~{}\\!\overline{p}\\!~{}\\}}{\tau^{\mathrm{SI}}}{\sqcup}~{}\delta_{2}=\forall
p_{\mathrm{leaf}}^{\Box}[\delta_{1}]\in\operatorname{leaves}(\delta_{1}:\tau^{\mathrm{SI}})~{}.~{}p_{\mathrm{leaf}}^{\Box}[\delta_{r}]=p_{\mathrm{leaf}}^{\Box}[\delta_{1}]\cup
p_{\mathrm{leaf}}^{\Box}[\delta_{2}]\cup\\{~{}\overline{p}~{}\\};\delta_{r}$
$\operatorname{assign\text{-}deps}(p:\tau^{\mathrm{SI}},\delta,\\{~{}\overline{p}~{}\\})=\forall{}p_{\mathrm{leaf}}^{\Box}[p]\in{}\operatorname{leaves}(p:\tau^{\mathrm{SI}})~{}.~{}p_{\mathrm{leaf}}^{\Box}[p]\mapsto{}p_{\mathrm{leaf}}^{\Box}[\delta]\cup{}\\{~{}\overline{p}~{}\\}$
$\operatorname{\delta\text{-}leaves}(\delta:\tau^{\mathrm{SI}})=\bigcup\operatorname{leaves}(\delta:\tau^{\mathrm{SI}})$

Figure 7. Selected metafunctions for manipulating dependencies

We elide the simple definition of the $\operatorname{leaves}$ metafunction,
which has a case for each of the syntactic forms an Oxide type might take.
$\operatorname{\delta\text{-}place}$ generates a $\delta$ which contains all
the dependencies of a place, retrieved from $\Pi$. Note that $\delta$ mirrors
the structure of the type of the place whose dependencies it models,
containing the same fields (specifically, leaves) as the type it corresponds
with. Each of these leaves of $\delta$ contains a set of dependencies. It is
treated as a place itself as a syntactic simplification; it should be thought
of as a map which is compatible with place expression contexts $p^{\Box}$. The
next metafunction,
$\delta_{1}\prescript{\\{~{}\\!\overline{p}\\!\\!~{}\\}}{\tau^{\mathrm{SI}}}{\sqcup}~{}\delta_{2}$,
acts as a union on a $\delta_{1}$ and a $\delta_{2}$ which correspond to the
same type, merging dependency sets between like leaves. An additional
parameter, $\\{~{}\overline{p}~{}\\}$, can be used to unconditionally add
dependencies to all leaves of the resulting $\delta$.

T-Move, then, generates a $\delta$ which represents the dependencies of a
place $\pi$, using it to represent the dependencies of the moved variable.
T-Copy functions analogously, taking into account that place expressions
(which may hold dereferences, see Fig. 5), not just places, may be copied. As
a result, it must use the ownership judgement (in the first premise) to
retrieve the dependencies of all the loans for the place expression $p$ to be
copied. A loan is any place expression which represents the same abstract
memory location as the place expression $p$, such as a dereference of a shared
reference to $p$. We use the $\sqcup$ operator to merge each loan’s generated
$\delta$ with the rest. Finally, T-Tuple demonstrates how $\delta$ is used
with place expression contexts $p^{\Box}$ in tracking dependencies.

####  A.1.2. Preventing flows

Σ; Δ; Γ; Θ; Π; Ψ; Ξ ⊢ e1: τ1SI∙ δ ⇒ Γ1; Π1Δ; Γ1; Θ ⊢+τ1SI↝ τaSI

$\vdash$

Γ1’ ∀ r ∈ free-regions(τaSI) . Γ1’ ⊢ r rnrb is-allowed(δ-leaves(δ: τSI) ∪ Ξ, {
x: τaSI}, Ψ) Π1’ = Π1[assign-deps(x: τaSI, δ, Ξ)] Σ; Δ; gc-loansΘ(Γ1’, x:
τaSI); Θ; Π1’; Ψ; Ξ ⊢ e2: τ2SI∙ δ’ ⇒ Γ2, x: τSD; Π2

1[T-Let] Σ; Δ; Γ; Θ; Π; Ψ; Ξ ⊢ let x: τ_a^SI = e_1; e_2: τ_2^SI  ∙ δ’ ⇒ Γ_2;
Π_2
Σ; Δ; Γ; Θ; Π; Ψ; Ξ ⊢ e: τSI∙ δ ⇒ Γ1; Π1Γ1(π) = τSXτSX= & r ω τXI⟹ r is unique
to π in Γ1Δ; Γ1$-$$\vartriangleright$ *π; Θ ⊢=τSI↝ τSX $\vdash$ Γ’ (τSX= τSD∨
Δ; Γ’; Θ ⊢uniqπ ⇒ { uniqπ }) Π2= Π1[assign-deps(π: τSI, δ, Ξ)] ∀ p□[π]:
τleafSI∈ leaves(π: τSI) . is-allowed(p□[δ] ∪ Ξ, { p□[π]: τleafSI}, Ψ)
1[T-Assign] Σ; Δ; Γ; Θ; Π; Ψ; Ξ ⊢ π:= e: unit ∙ ∅ ⇒ Γ’[π ↦ τ^SI], Π_2

Figure 8. Selected rules responsible for checking flows

A second selection of rules, presented in Fig. 8, is responsible not only for
tracking flows, but for preventing them when needed. The first is T-Let, which
provides the base case for information flow— all dependencies tracked
throughout the system originate here. In order to explain T-Let, we introduce
our final set of metafunctions. $\operatorname{assign\text{-}deps}$ takes a
place $p$, its $\delta$, and a set of dependencies as arguments, and adds
those dependencies to each leaf of $p$; it is used to update a place’s entry
in $\Pi$. $\operatorname{\delta\text{-}leaves}$ gathers all the dependencies
from a $\delta$, unioning the dependency sets from its leaves. Finally,
$\operatorname{is\text{-}allowed}$ (shown in Fig. 10) takes a set of sources,
a set of destinations, and a flow policy set $\Psi$ as arguments, and checks
that each of the sources is allowed to flow to each of the destinations,
succeeding if all of the flows are allowed. It relies on
$\operatorname{get\text{-}min\text{-}perms}$ (shown in Fig. 10) to search
$\Psi$ for the correct flow policy to apply, which it does according to the
overriding policy discussed in Fig. 2. To do this, it relies on $+\\!\\!>$, a
reflexive and transitive binary relation on access expressions $a$ which will
succeed if the first access expression syntactically represents access to the
second one. $p~{}+\\!\\!>p.f$ and $*~{}+\\!\\!>p$ define success.

$\displaystyle\operatorname{is\text{-}allowed}(\\{~{}\overline{p_{1}:\tau_{1}^{\mathrm{SI}}}~{}\\},\\{~{}\overline{p_{2}:\tau_{2}^{\mathrm{SI}}}~{}\\},\Pi,\Psi)=$
$\displaystyle\quad\forall(p_{1}:\tau_{1}^{\mathrm{SI}},p_{2}:\tau_{2}^{\mathrm{SI}})\in{}\\{~{}\overline{p_{1}:\tau_{1}^{\mathrm{SI}}}~{}\\}\times{}\\{~{}\overline{p_{2}:\tau_{2}^{\mathrm{SI}}}~{}\\}~{}.$
$\displaystyle\quad((\\_,\\_,\texttt{true})=\operatorname{get\text{-}min\text{-}perms}(p_{1},p_{2},\Psi))$
Figure 9. Checks if flows are allowed

$\displaystyle\operatorname{get\text{-}min\text{-}perms}(p_{1},p_{2},\Psi)=$
$\displaystyle\quad\\!\operatorname{foldr}(((a_{2},a_{3},\beta_{1}),(a_{4},a_{5},\beta_{2}))\rightarrow$
$\displaystyle\quad\quad\text{if}~{}a_{2}~{}+\\!\\!>{}p_{1}\wedge{}a_{3}~{}+\\!\\!>p_{2}~{}\wedge$
$\displaystyle\quad\quad\quad((a_{4}~{}+\\!\\!>{}a_{2}\wedge{}a_{5}~{}+\\!\\!>{}a_{3})~{}\lor$
$\displaystyle\quad\quad\quad((a_{4}~{}+\\!\\!>{}a_{2}\lor{}a_{5}~{}+\\!\\!>{}a_{3})\wedge{}\beta_{1}=\texttt{false}))$
$\displaystyle\quad\quad\text{then}~{}(a_{2},a_{3},\beta_{1})$
$\displaystyle\quad\quad\text{else}~{}(a_{4},a_{5},\beta_{2}),$
$\displaystyle\quad(*,*,\texttt{true}),\Psi)$ Figure 10. Retrieves a maximally
precise rule from $\Psi$

Given these definitions, T-Let checks if the dependencies of the expresssion
$e$ to be bound, as well as any branch dependencies, are permitted to flow to
the variable to be bound, according to the current flow policy. Additionally,
it gives the bound variable the expression’s dependencies by updating $\Pi$.
Similarly, T-Assign updates the assignee’s dependencies in the dependency
environment with those of the expression being assigned, along with any
dependenies from control flow. It then checks whether flows are allowed from
each leaf of the assignee from the relevant dependencies of the expression
being assigned.

We now briefly discuss our handling of function application, eliding typing
rules for brevity. Note that we change Oxide’s function call form, removing
the return value— any program which uses function return values may be
transformed to a program which returns information through a mutable reference
passed to the function. This simplifies information flow checking for function
calls. Like (Crichton et al., 2022), our system is modular, opting to preserve
abstraction at the cost of precision. When a function call is encountered, we
first retrieve the flow policies declared by the function which are valid for
its entire scope, in addition to any policies permitting flows, adding them
all to a new $\Psi$ representing the function’s flow policy set. We then
substitute the function call’s actual parameters for its formal parameters
within this $\Psi$, and compare it to the $\Psi$ for the calling context. If
the calling context’s $\Psi$ implies the one generated for the function call,
then no error is raised. Specifically we check that, for all the mutable
references passed to the function, any flow permitted by the function to that
unique reference is also permitted by the calling context. We exclusively
consider uniq refs because they are the only means by which information may
escape our function call form, and violate the calling context’s information
flow policies.

The typing rules for the flow  and allow constructs are straightforward, so
we also elide their definitions for brevity. When a flow policy is declared,
it is added to the current flow policy environment $\Psi$. Flow policies may
be declared between access expressions; for any access expression which is not
*, the ownership judgement is used to ensure that the place expression is
accessible. When allow is used on an expression $e$ of type $\tau$, it returns
a $\delta$ with all of its leaves (according to $\tau$) set to
$\varnothing{}$.


# Checkpoint-Restart Libraries Must Become More Fault Tolerant

Anthony Skjellum  University of Tennessee at Chattanooga
Tennessee, USA
<EMAIL_ADDRESS>Derek Schafer  University of Tennessee at Chattanooga
Tennessee, USA
<EMAIL_ADDRESS>
###### Abstract

Production MPI codes need checkpoint-restart (CPR) support. Clearly,
checkpoint-restart libraries must be fault tolerant lest they open up a window
of vulnerability for failures with byzantine outcomes. But, certain popular
libraries that leverage MPI are evidently not fault tolerant. Nowadays, fault
detection with automatic recovery without batch requeueing is a strong
requirement for production environments. Thus, allowing deadlock and setting
long timeouts are suboptimal for fault detection even when paired with
conservative recovery from the penultimate checkpoint.

When MPI is used as a communication mechanism within a CPR library, such
libraries must offer fault-tolerant extensions with minimal detection,
isolation, mitigation, and potential recovery semantics to aid the CPR’s
library fail-backward. Communication between MPI and the checkpoint library
regarding system health may be valuable. For fault-tolerant MPI programs
(e.g., using APIs like FA-MPI, Stages/Reinit, or ULFM), the checkpoint library
must cooperate with the extended model or else invalidate fault-tolerant
operation.

###### Index Terms:

checkpoint-restart, fault-tolerance, MPI

##  I Introduction

Having MPI jobs killed and re-queued at the tail of their specific job queue
(using a previous checkpoint) is undesirable when it can be avoided; fault-
tolerant extensions to MPI are designed, in some cases, to avoid this
situation (e.g., [1]). This recovery mode introduces significant and unwanted
delays when faults can be managed. But, if checkpoint-restart (CPR) libraries
for MPI applications are not themselves fault tolerant, they expose MPI
programs to secondary risks of byzantine failures. Further, there is no
guarantee that fail-stop occurs. Deadline can occur, and, unless the
application is actively monitored, or has a global time-out switch, it will
simply waste the remainder of its scheduled allocation.

CPR libraries that use MPI need to collaborate with the MPI implementation, at
least minimally, to support fail backward and avoid deadlocks when failures
occur during their control of the parallel program. They must also collaborate
with the fault-tolerance model used in an MPI program augmented with a
specific set of fault-tolerant extensions. The fault-tolerant MPI model of the
CPR library has to be appropriate to that fault-tolerance model, and not be
incompatible with any and all fault-tolerant actions taken by the application.
Otherwise destructive interference between the concerns will occur, and
prevent them from collaborating during detection, isolation, mitigation, and
recovery. Fault tolerant models that use a checkpoint-restart library to
checkpoint MPI state, in addition to application state, add to the importance
of resilience of the checkpoint-restart library itself. This use case may pose
other requirements too.

The remainder of this short paper is organized as follows: Section II
identifies issues and concerns about fault-tolerance in a CPR library, its
interactions with MPI, as well as interactions with the MPI application.
Section III offers straightforward next steps to advance CPR libraries.
Conclusions and some future work are discussed in Section IV.

##  II Identifying the Issues

Multiple fault-tolerant models appear to be inherent if checkpoint-restart is
employed with a fault-tolerant model (which is common) and the CPR library
also utilizes MPI (which varies between different products). Only if a given
checkpoint library is MPI-free can one evidently avoid the multiple MPI fault-
tolerant model issue.

One upshot of fault tolerance within the CPR library is that, if a given MPI-
dependent checkpoint library uses one specific model only, then that model
fixes what the application may itself use. Alternatively, a given CPR library
would have to be configurable for each kind of support fault-tolerant model
used in a set of production applications, which would be expensive to code,
validate, and maintain.

For instance, with MPI Stages (a Reinit-type model) [1, 2], the approach is to
quiesce MPI and then call the checkpoint library for application state
preservation plus optional MPI-Stages-related serialization strings for future
recovery; then, the approach is to call a separate MPI-Stages internal state
checkpoint (including application objects serialized). This concept of
operations apparently does not contemplate that the CPR library actually uses
MPI itself, thereby changing the internal state of MPI. Further, if a fault
occurs during this checkpoint procedure, it is not guarded by a resilient MPI
mode of operation that may detect faults/failures and provide potential for an
isolation, mitigation, or recovery process. Such a failure window diminishes
the benefit of the MPI Stages (or other fault-detecting operational model or
system). In short, the application could still crash, abort, or deadlock.

Whenever a CPR library uses MPI, it should use the fault-tolerance extensions
available to that MPI implementation, or at least work within standard MPI’s
ability to return error codes and assess continuability after errors. In
particular, a CPR library’s use of MPI will need to utilize a) a fault
detection mechanism, b) a fault-friendly means to reach consensus between peer
processes in the given MPI communicator’s scope (or the entire world of
processes), c) a means to cause the MPI session to fail-backward, and, d) a
way to pass back error information to the application, if the application
should commit to the fail-backwards itself (likely). A CPR library’s specific
fault-tolerant syntax and semantics will either have to match the
application’s or run in a mode where multiple, interoperable fault-tolerant
libraries are present. This introduces the fault-tolerant-library concern that
real applications have, even though it is part of defensive I/O to support
fault tolerance itself. Further, if the checkpoint library uses MPI I/O rather
than POSIX I/O, then the entire MPI I/O feature set used has to be fault
tolerant as well, which is a heavy lift in terms both of specification and
implementation.

A reasonable fault-tolerance model for a CPR library would be as follows,
leveraging MPI’s C interface, errors-return mode, and some nominal FT
extension(s) in any of the common models111 ULFM [3], Reinit [1], MPI Stages
[2, 4], and FA-MPI [5] are deemed common models since discussed in the MPI
Forum’s Fault Tolerance Working Group.:

  * •

require that the MPI program be initialized to use MPI_Errors_return and
sample all return codes

  * •

use fault-tolerant allgathers or reductions to achieve consensus on error
state among surviving processes

  * •

take one of these two actions:

    1. 1.

return a meaningful error code (across all surviving processes) to the
application so that the application realizes it must activate its own fault
tolerance mode. The application has to interpret that code in terms of the
fault tolerant model it is itself using.

    2. 2.

directly initiate recovery in the same model that the application uses222It
will probably be needed to code variations into the CPR library, but it seems
expensive at this time to force the library to have a new, manual coding
approach for every application FT mode chosen.

An alternative to the error-return code is to recompile the CPR library with
C++, while still using the MPI C interface, but augmenting it with additional
C++ features that provide fault-tolerant extensions (e.g., exceptions)[6]. In
this way, a group-wide parallel containment domain could be supported and the
CPR library could determine consensus in that containment domain, and then
simply rethrow the exception to the application. A common parallel containment
domain methodology usable with C++ and Stages or FA-MPI appears doable at
present, meaning that the CPR library would be recoded once to support either
model. ULFM as currently evolving in the MPI Forum may also be applicable.

At least, one would need to provide the following to make the MPI usage inside
a checkpoint library “ready” for use in conjunction with the application’s
fault-tolerance model:

  * •

All collective routines must be able to work in a fault-tolerant mode, so they
do not deadlock when a network error occurs or a process hangs or fails333Such
a mode of operation is being considered at present in the Fault Tolerant
Working Group of the MPI Forum.;

  * •

A mechanism of consensus for the health state (failed, good, unknown) must be
delivered to the CPR library whenever a collective operation it initiates
fails.

  * •

If there should be errors in point-to-point operations, the CPR library must
be able to invoke a consensus-type collective operation to determine the state
of the MPI communicator (usually MPI_COMM_WORLD).

  * •

If the CPR library uses MPI I/O, then the MPI I/O library must be minimally
fault tolerant with regard to returning errors codes, not deadlock with dead
or hung processes, and time out when I/O services become unresponsive.

In all cases, we expect that such failures detected at the CPR library level
will generate one of these actions:

  * •

fail-upward back to the MPI application, so it returns from checkpoint with
consensus to stop running and uses a Reinit-type decision and recovers
(without re-queueing by the job scheduler) with an earlier checkpoint

  * •

directly cause the application to do the Reinit-type operation as a policy of
the checkpoint library

  * •

kill/abort the application, and let it be restarted by the job scheduler with
an earlier checkpoint. (As noted, this is the most expensive option from the
user’s viewpoint.)

Interactions between the CPR library and MPI implementation also appear to
have merit for future consideration in failure modes. For instance, overhead
reductions could be possible.

##  III Path Forward

A key next step appears to be a careful review of how popular CPR libraries
use MPI in detail as a first step to adding fault-tolerant extensions to them.
The choice of fault-tolerant modes of these libraries will either need to
reflect the choice of a single overarching fault-tolerant mode for MPI, or
else support multiple ones. Prototyping fault-tolerant extensions within a CPR
library like SCR [7] appears warranted at present, with demonstration of
overall resilience when coupled with a fault-tolerant MPI program.

What has noted been noted so far is that these libraries use MPI, but do
nothing overt to change error-handlers, sample MPI API return codes, or
exploit fault-tolerant extensions: SCR [7] and MANA [8]. We noted that BLCR
and DMTCP [9, 10] do not use MPI directly. Without having yet evaluated its
performance or examined its implementation, the meta-CPR library CRAFT [11]
describes using SCR and ULFM together for fault-tolerant operation, and is
exemplary of what this paper proposes as a baseline requirement set/approach
for CPR libraries.

Transparent CPR libraries (e.g., DMTCP [10] and MANA [8]) may use MPI in ways
that introduce deadlock when an MPI operation fails. Careful study of how
transparent checkpointing interacts with a fault-tolerant model of MPI is also
warranted. Two-way communication between a fault-tolerant MPI and a
transparent CPR library appears useful for reduced overheads too.

Lastly, CPR libraries must minimally become aware of new error information and
the pre-MPI_Init ability to set error handlers supported by MPI-4, as well as
MPI Sessions. The paper by Skjellum et al., considers fault-tolerance and
Sessions [12]. This paper also suggests an extended execution model for fault-
tolerant MPI programs; that explicit scaffolding could also be useful for
exploitation by CPR libraries as well, particularly to help automate
unsupervised fallback recovery without batch requeueuing.

##  IV Conclusion

This short paper discussed and motivated the need for checkpoint-restart (CPR)
libraries to become more fault tolerant when used in conjunction with MPI
applications and libraries. Further requirements are posed on the library when
the MPI program is extended with fault-tolerant extensions.

It is well known that checkpoint-restart libraries must be fault tolerant, not
just deadlock or timeout, or else they open up a window of vulnerability for
failures to occur with byzantine outcomes. But, certain popular libraries that
leverage MPI are evidently not fault tolerant. Nowadays, fault detection with
automatic recovery without batch requeueing form a strong requirement for
production environments. Thus, allowing deadlock and relying on long timeouts
for fault detection is a suboptimal strategy even when paired with
conservative, but common recovery policy of using the penultimate checkpoint,
rather than a the last checkpoint (which might have been compromised by a
fault during creation).

When MPI is used as a communication mechanism within a CPR library, such
libraries must integrate fault-tolerant extensions with minimal detection,
isolation, mitigation, and potential recovery semantics to aid the CPR’s
library fail-backward. Communication between MPI and the checkpoint library
regarding system health may be valuable. For fault-tolerant MPI programs
(e.g., using APIs like FA-MPI, Stages/Reinit, or ULFM), the checkpoint library
must cooperate with the extended model or else invalidate fault-tolerant
operation, even if they don’t use MPI directly at present.

Carefully evaluating how CRAFT [11] works with and integrates SCR [7] and ULFM
[3], then extrapolating how it could work with other fault tolerant models of
MPI, will be among the future work to be explored. Refining the set of
interoperability requirements and data interchanges needed for Reinit/Stages
and FA-MPI to work well with a CPR library is also planned as extensions to
the principles described more generally here. Determining whether CPR
libraries pose new, implicit and/or previously unfulfilled requirements on
fault-tolerant models of MPI will also be considered.

## Acknowledgments

The authors wish to thank the anonymous reviewers, whose feedback helped
improve the final document.

This work was performed with partial support from the National Science
Foundation under Grants Nos. 1822191, 1918987, 1925538, and 1925603. Any
opinions, findings, and conclusions or recommendations expressed in this
material are those of the authors and do not necessarily reflect the views of
the National Science Foundation.

## References

  * [1] G. Georgakoudis, L. Guo, and I. Laguna, “Reinit++: Evaluating the performance of global-restart recovery methods for mpi fault tolerance,” 2021.
  * [2] N. Sultana, M. Rüfenacht, A. Skjellum, I. Laguna, and K. Mohror, “Failure recovery for bulk synchronous applications with MPI stages,” _Parallel Computing_ , vol. 84, pp. 1 – 14, 2019. [Online]. Available: http://www.sciencedirect.com/science/article/pii/S0167819118303260
  * [3] W. Bland, A. Bouteiller, T. Herault, J. Hursey, G. Bosilca, and J. J. Dongarra, “An evaluation of user-level failure mitigation support in MPI,” in _Recent Advances in the Message Passing Interface_ , J. L. Träff, S. Benkner, and J. J. Dongarra, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, pp. 193–203.
  * [4] D. Schafer, I. Laguna, A. Skjellum, N. Sultana, and K. Mohror, “Extending the MPI stages model of fault tolerance,” in _2020 Workshop on Exascale MPI (ExaMPI)_. IEEE, 2020, pp. 52–61.
  * [5] A. Hassani, A. Skjellum, P. V. Bangalore, and R. Brightwell, “Practical resilient cases for fa-mpi, a transactional fault-tolerant MPI,” in _Proceedings of the 3rd Workshop on Exascale MPI, ExaMPI@SC 2015, Austin, Texas, USA, November 15, 2015_. ACM, 2015, pp. 1:1–1:10. [Online]. Available: https://doi.org/10.1145/2831129.2831130
  * [6] M. Ruefenacht, D. Schafer, A. Skjellum, and P. V. Bangalore, “MPI’s language bindings are holding MPI back,” _CoRR_ , vol. abs/2107.10566, 2021. [Online]. Available: https://arxiv.org/abs/2107.10566
  * [7] A. Moody, G. Bronevetsky, K. Mohror, and B. R. d. Supinski, “Design, modeling, and evaluation of a scalable multi-level checkpointing system,” in _Proceedings of the 2010 ACM/IEEE International Conference for High Performance Computing, Networking, Storage and Analysis_ , ser. SC ’10. USA: IEEE Computer Society, 2010, p. 1–11. [Online]. Available: https://doi.org/10.1109/SC.2010.18
  * [8] R. Garg, G. Price, and G. Cooperman, “MANA for MPI: MPI-agnostic network-agnostic transparent checkpointing,” in _Proc. of the 28th Int. Symp. on High-Performance Parallel and Distributed Computing_. ACM, 2019, pp. 49–60.
  * [9] P. H. Hargrove and J. C. Duell, “Berkeley lab checkpoint/restart (blcr) for linux clusters,” in _Journal of Physics: Conference Series_ , vol. 46, no. 1. IOP Publishing, 2006, p. 067.
  * [10] J. Ansel, M. Rieker, and G. Cooperman, “User-level socket-based checkpointing for distributed and parallel computation,” _CoRR_ , vol. abs/cs/0701037, 2007\. [Online]. Available: http://arxiv.org/abs/cs/0701037
  * [11] F. Shahzad, J. Thies, M. Kreutzer, T. Zeiser, G. Hager, and G. Wellein, “Craft: A library for easier application-level checkpoint/restart and automatic fault tolerance,” _IEEE Transactions on Parallel and Distributed Systems_ , vol. 30, no. 3, pp. 501–514, 2019.
  * [12] A. Skjellum, D. Schafer, and I. Laguna, “MPI Sessions and fault tolerance: A position paper,” September 2021, EuroMPI 2021, in press.
  * [13] R. B. Brightwell, A. Hassani, and A. Skjellum, “Comparing contrasting generalizing and integrating two current designs for fault-tolerant MPI.” 9 2014. [Online]. Available: https://www.osti.gov/biblio/1314607