11institutetext: University of Birmingham, UK
22institutetext: Fetch.ai
22email<EMAIL_ADDRESS><EMAIL_ADDRESS>
# SoK: Untangling File-based Encryption on Mobile Devices

David Galindo 1122 Jia Liu 22 Chris McMahon Stone 11 Mihai Ordean 11

###### Abstract

File-based encryption (FBE) schemes have been developed by software vendors to
address security concerns related to data storage. While methods of encrypting
data-at-rest may seem relatively straightforward, the main proponents of these
technologies in mobile devices have nonetheless created seemingly different
FBE solutions. As most of the underlying design decisions are described either
at a high-level in whitepapers, or are accessible at a low-level by examining
the corresponding source code (Android) or through reverse-engineering (iOS),
comparisons between schemes and discussions on their relative strengths are
scarce. In this paper, we propose a formal framework for the study of file-
based encryption systems, focusing on two prominent implementations: the FBE
scheme used in Android and Linux operating systems, as well as the FBE scheme
used in iOS. Our proposed formal model and our detailed description of the
existing algorithms are based on documentation of diverse nature, such as
whitepapers, technical reports, presentations and blog posts, among others.
Using our framework we validate the security of the existing key derivation
chains, as well as the security of the overall designs, under widely-known
security assumptions for symmetric ciphers, such as IND-CPA or INT-CTXT
security, in the random-oracle model.

##  1 Introduction

In the last decade mobile devices have become an integral part of modern life.
As a result more and more sensitive data is accumulated on these devices which
have become targets for third parties.

As a response to these potential dangers, the smartphone industry has designed
mechanisms to secure their customers devices, starting with securing access
control with mandatory user authentication mechanisms, from biometrics and
passcodes, all the way through to protecting the data stored on the devices
using file encryption systems. This has however led to a number of
controversies such as the 2016 San Bernadino ”FBI vs Apple” case in which the
FBI demanded (unsuccessfully) from Apple to undermine their existing iOS
security features by implementing backdoors that would allow government
officials to access encrypted data under specific circumstances [1, 14].

Technical documents resulting from this case, as well as some more recent
studies [25], have revealed significant gaps with respect to understanding the
technical details of the security features implemented in these devices. This
arises from the fact that often these features are only presented in
whitepapers which brush over relevant technical details in favour of high
level descriptions, e.g. [2, 37]. Although alternative methods such as source
code reviewing are in principle possible, these are in most cases hindered by
the manufacturers’ preference towards closed source software. Thus, more often
than not, true insight only becomes possible after significant reverse
engineering campaigns [39]. In order to bridge these gaps multiple
comprehensive studies about mobile device security have been done [42, 40,
44], however their main focus has been on providing details about the inner
workings of the analysed schemes.

###  1.1 Contributions

In this paper we take a different approach, where we propose a new generic
formalisation for File-Based Encryption (FBE) schemes with the goal of making
existing and future schemes easier to analyse. In order to develop our
formalisation we aggregate available information about FBE from multiple
knowledge domains including whitepapers, technical documents, published source
code and reverse engineering results ([17, 2, 15, 37, 19], [21], [20, 34, 33],
[26, 29, 12, 19]).

We carry out a formal analysis of the designs and implementations of FBE
schemes, whilst also drawing up a comparison of the varying security
guarantees that each implementation provides. More concretely, we provide:

  1. 1.

A formalisation of FBE schemes

  2. 2.

Generic adaptations using our formalism of the main FBE schemes used by
Android and iOS, as reconstructed from multiple knowledge domains

  3. 3.

An up-to-date security analysis for the schemes used in Android and iOS

In our analysis we target the main processes that enable FBE schemes to work,
which we group in two categories: C1) the key derivation methods, and root of
trust placement and C2) file encryption and decryption algorithms. For
algorithms and methods in C1) we provide complete generic descriptions, in
Sections 3-5, and specific analysis for both Android and iOS. We found that
algorithms from this category have atypical implementations which mostly arise
from hardware limitations or user interaction requirements. Therefore, where
appropriate, we also consider functionality that depends on user inputs, such
as passcodes or biometrics, to secure the keys that protect the memory storage
of the device. Algorithms in C2) follow the standard practices for FBE. We
cover these in Section 6 for Android and *NIX systems only, due to limited
availability of appropriate low-level documentation for iOS. We argue that our
findings will allow manufacturers to accurately pinpoint the components which
have the biggest impact on the security of the device and allocate more
resources towards securing these. Conversely, this work also allowed us to
identify attack scenarios which do not directly translate to compromising the
whole security of the device.

##  2 File-based encryption security

In this section we will give the syntax for a generic $MobileFBE$ scheme,
followed by a definition of the corresponding security policies.

###  2.1 Scheme definitions.

###### Definition 1

A _MobileFBE scheme 111We sometimes use the terms scheme and protocol
interchangeably._ with a defined set of policies $\mathcal{P}$ is a tuple of
eight polynomial-time algorithms
$\mathsf{MFBE}{}=\allowbreak(\allowbreak\mathsf{KGen},\allowbreak\mathsf{WrapKey},\allowbreak\mathsf{UnwrapKey},\allowbreak\mathsf{ProvisionKey},\allowbreak\mathsf{EvictKey},\allowbreak\mathsf{VerifyToken},\allowbreak\mathsf{Encrypt},\allowbreak\mathsf{Decrypt})$
such that:

$k\leftarrow\mathsf{KGen}(1^{\lambda}):$

is a probabilistic algorithm for generating $\mathsf{MFBE}{}$ class keys. It
takes as input the security parameter $\lambda$ and outputs a random value $k$
of length $\lambda$.

$\\{\phi,\overline{pol}\\}\leftarrow\mathsf{WrapKey}^{\sigma}(k,\omega,pol):$

is a probabilistic algorithm that takes as input an unencrypted key $k$, an
encrypted wrapping key $\omega$, and a unbound policy $pol$. The policy $pol$
contains information related to the intended usage of key $k$ and the ciphers
used to encrypt it. The algorithm returns $\phi$, an encryption of $k$ with
respect to $\omega$, and $\overline{pol}$ the policy $pol$ bound with the
wrapping key $\omega$.

($k,\bot)\leftarrow\mathsf{UnwrapKey}^{\sigma}(\phi,\overline{pol}):$

is a deterministic algorithm that takes as input an encrypted key $\phi$ and a
bound policy $\overline{pol}$. It returns a file encryption key $k$ obtained
by decrypting $\phi$ with the wrapping key bound in $\overline{pol}$.
Depending on the cipher used in the policy $\bot$ may returned if the
decryption is not successful.

$kid\leftarrow\mathsf{ProvisionKey}(k):$

is a deterministic algorithm to provision keys for their usage. It takes as
input a key $k$ and outputs an identifier $kid$ of the key thus installed.

$\\{1,\bot\\}\leftarrow\mathsf{EvictKey}(kid):$

is a deterministic algorithm used to discard keys. It takes as input the key
identifier $kid$ to be discarded from memory and outputs $1$ if the operation
was successful or $\bot$ otherwise.

$\\{1,\bot\\}\leftarrow\mathsf{VerifyToken}(authToken):$

is a deterministic algorithm used to verify the validity of a
cryptographically generated token $authToken$. It returns $1$ if the token
verification was successful or $\bot$ otherwise.

($e{\textit{f}}node,\bot)\leftarrow\mathsf{Encrypt}({\textit{f}node},kid):$

is a probabilistic algorithm to encrypt a FBE filesystem node (e.g. file or
file directory). It takes as input the node, ${\textit{f}}node$, and a key or
key id, $kid$; outputs its encrypted counterpart, $efnode$. It may return
$\bot$ if the identifier $kid$ is not valid.

(${\textit{f}}node,\bot)\leftarrow\mathsf{Decrypt}(e{\textit{f}}node,kid):$

is a deterministic algorithm to decrypt a FBE encrypted node. It takes as
input the encrypted node, $e{\textit{f}}node$, and a key or key id, $kid$;
outputs its decryption, ${\textit{f}}node$. It may return $\bot$ if the
decryption was not successful (i.e. invalid key or $kid$).

##  3 Preliminaries

In this section we focus on the syntax of security policies and how we use
them to accurately describe existing key policies used in mobile operating
systems.

###  3.1 Generic syntax of security policies

We use the notion of a security policy to express (1) the usage scenarios
allowed for keys in a MobileFBE scheme, and (2) the security parameters
required for the management of these keys. These policies describe how and
when keys are built, provisioned and stored. The security parameters within
the policy also dictate relationships between keys. This allows us to capture
details such as whether a key is cryptographically bound to an external
process or device, e.g. the Secure Enclave Processor in iOS. As such, a
generic policy is defined as a tuple of four parameters:

$pol=[cipher,wrappingKey,authToken,usage]$

We distinguish two types of policies: unbound policies $pol$ which are
associated to new, unprotected file encryption keys, i.e. $(k,pol)$ and bound
policies $\overline{pol}$ associated to protected file encryption keys, i.e.
$(\phi,\overline{pol})$. The unbound policies do not yet contain any
cryptographic material specific to a device or credential, such as wrapping
keys or authentication tokens. When platform specific cryptographic material
is added to the policy, the policy becomes bound to said platform and is
denoted as $\overline{pol}$. The keys and parameters of the bound policy
$\overline{pol}$ are used to protect the file encryption key associated to the
policy (i.e. $\phi$) and restrict use of that key to that specific platform.

_The $cipher$ parameter._ This parameter specifies the cipher and parameters
that were used to encrypt the key $k$ to which the policy is associated. We
use standard notation to describe this (e.g. AES-256-GCM: AES cipher with a
key of length 256bits and a GCM block chaining mode).

_The $wrappingKey$ parameter._ It refers to the ciphertext that contains the
private key under which the key $k$ associated to a policy is encrypted. On
platforms that have access to a trusted execution environment (TEE) the
wrapping keys are encrypted with hardware bound keys that are exclusively
stored inside the TEE. This ensures that recovery of the file encryption key
cannot be done without access to the TEE. This also enforces verification of
the policy inside the TEE. For platforms lacking a TEE wrapping keys are still
used as they are part of the code base, but they will not provide any
additional security benefits. It is worth noting that mobile platforms without
TEEs are rare in practice nowadays.

_The $authToken$ parameter._ The authToken or authentication token is a
platform specific, optional cryptographic value that encodes the user
contribution (e.g. password, PIN, fingerprint reader output) in the form of a
specific cryptographic hash (in Android), or a password derived key (in iOS).
If the value is null then decrypting the key file encryption key $k$ can be
done transparently, without any input from the user. We discuss this further
in the next section.

_The $usage$ parameter._ This final parameter is used to indicate the purposes
and restrictions associated with the use of a key.

###  3.2 The authToken

Android. In Android, the user input, e.g. the user passphrase or PIN, is
encoded as a data structure refered to as AuthToken [16]. The AuthToken token
generation and verification consists of two parts and is managed by the
Gatekeeper trustlet in the TEE and a counterpart service running on the
insecure application processor. During the enrolment phase (e.g. on first
boot) a 64-bit user secure identifier, named AuthToken HMAC Key, is created by
Gatekeeper trustlet and is then shared between all the relevant TEE
components, namely the Gatekeeper, Keymaster and biometric trustlet. On
subsequent operations which require user authentication, the Gatekeeper
service running on the application processor will generate AuthTokens which
need to be included as part of any requests. The submitted tokens are verified
inside the TEE by the Keymaster trustlet which handles key management and
verifies tokens related to FBE keys. Rate limiting of authentication attempts,
based on time-delays as well as token freshness and correctness are enforced
by the TEE trustlet [16].

iOS. A similar functionality for handling user input exists in iOS, however it
is enforced through encryption rather than MAC verification. A wrapping key
$k_{master\\_key}$ is derived inside the secure enclave processor (SEP) from
the user input using a key derivation function. The derivation process
enforces time-delayed rate limiting and, as such, the $k_{master\\_key}$ will
have the same security protections against brute-force attacks as the Android
AuthToken equivalent [26].

Due to the similarity in functionality, security properties and usage, we
refer to both the Android’s AuthToken and iOS’s $k_{master\\_key}$ with the
generic term authToken throughout the rest of the paper, and we make the
distinction where relevant.

###  3.3 Android policies

Since the introduction of FBE in Android 7.0, there has been support for two
main encryption contexts, called Device Encrypted (DE) and Credential
Encrypted (CE). The former of the two protects data up until the point at
which a successful Verified Boot222Verified boot guarantees the integrity of
the Android OS software with hardware backed root of trust binding [18]. has
taken place. The latter, which is the default storage location, makes data
available once a user has unlocked the device for the first time, up until the
device has been shut down [17]. Data in both the DE and CE storage locations
is encrypted with keys that are protected with trusted hardware. In Android,
the trusted hardware consists of a Key management applet, named Keymaster,
which runs in a secure enclave in ARM TrustZone.

_The $DE_{s}$ policy._ The device encryption context is split into two
policies. The first policy is called $DE_{s}$, and describes when and how
system data is encrypted. This policy protects storage areas that are
associated with the device and that are common for all enrolled users. This
includes, for example, Wi-Fi credentials and Bluetooth pairing data [15].
Using our syntax, the policy $DE_{s}$ associated with the key $\phi_{DEs}$ is:

$\footnotesize
DE_{s}=[\text{{AES-256-GCM}},\omega_{DEs},null,DeviceDataAfterBoot],$

where $\omega_{DEs}$ is the hardware bound ciphertext of the key used to
protect $\phi_{DEs}$. Keys associated with this policy do not require any user
input in order to be made available, and as such the authentication token is
set to $null$.

_The $DE_{u}$ policy._ The second DE policy is the per-user context policy
$DE_{u}$. Data encrypted under this policy is user specific, but is made
available along with $DE_{s}$ data after boot without requiring any
contribution from the user to enable usage. It includes data such as alarms,
wallpapers and active ring tones [15]. There is a separate $DE_{u}$ master key
for each enrolled user, where $u$ is the user id. Cryptographically speaking,
the $DE_{u}$ policy is identical to $DE_{s}$, the only difference being the
usage parameter:

$\footnotesize
DE_{u}=[\text{{AES-256-GCM}},\omega_{DEu},null,UserDataAfterBoot],$

where $\omega_{DEu}$ is a unique hardware bound ciphertext specific to each
$\phi_{DEu}$.

_The $CE_{u}$ policy._ The $CE_{u}$ policy describes the credential encrypted
context in Android. This is also a per-user encryption context. However,
unlike $DE_{u}$, this context ensures data is protected until after first
authentication. This is the default policy for all user data, and includes
files like documents, photos and app data. Similar to the $DE_{u}$ policy,
there is a separate $(\phi_{CEu},CE_{u})$ key-policy pair for each user.
Because files encrypted in this context are only decrypted after a successful
user authentication, a verified authentication token $AuthToken$ is required
by the Keymaster element to unwrap and install the $CE_{u}$ key. The policy
can be represented as:

$\footnotesize CE_{u}=[\text{{AES-256-GCM}},\omega_{DEu},\\\
AuthToken,UserDataAfterAuth]$

where $\omega_{CEu}$ is a unique hardware bound ciphertext specific to each
$\phi_{CEu}$, and $AuthToken$ is a cryptographic hash generated inside the
TEE.

_Other keys._ Support for metadata encryption has been introduced since
Android 9. Under the current implementation model, data that is not already
protected by the $DE$ or $CE$ keys, (e.g. file sizes, permissions) is
considered to be metadata and is encrypted using a separate key, which we
denote $k_{metadata}$. The metadata protection is implemented as a
supplementary full disk encryption layer, i.e. an adaptation of Android 5.0
full disk encryption [19] that has been previously analysed in [40].

###  3.4 iOS policies

Apple introduced its implementation of hardware-backed file-based encryption
with iOS 4 in 2010 under the name Data Protection. In the latest version of
Data Protection, four primary encryption contexts are supported — classes A to
D. In reverse order, ClassD is the Android $DE_{s}$ equivalent and ClassC is
the Android $CE_{u}$ equivalent. Unlike Android, iOS does not support
cryptographic separation of per-user file system content (i.e. per-user
$DE_{u}$), nor does it support multiple user profiles per device (i.e. more
than one $CE_{u}$) [2, 11]. Two additional policies are supported in iOS:
ClassB, which allows writing encrypted data but not reading whilst a device is
locked; and ClassA, which evicts corresponding keys from memory when a device
is locked after a successful authentication [2]. All keys in this scheme are
bound to the Secure Enclave Processor (SEP). Like Android, all class keys are
wrapped using AES-256-GCM [5]. However, unlike Android, in iOS all keys are
generated and stored inside the SEP and all relevant encryption and decryption
operations are run either by the SEP or by the specific hardware which
intermediates access to the data (e.g. the storage controller). According to
Apple, keys are never released into the main memory of controlled by the
application processor [2]. Additionally, in iOS class keys are used not only
to encrypt files but also to encrypt other class keys which have a more
restrictive usage. Below we show how our proposed syntax can be used to model
the iOS security policies.

_$ClassD$ policy._ Data protected under this policy consists primarily of
system files needed for boot, but also Voicemail, Bluetooth and iMessage keys,
VPN certificates, etc. As this is one of the most permissive keys in iOS it is
only protected with the hardware key of the TEE (i.e. a unique 256bit AES key,
fused into the SEP during manufacturing). The ClassD policy associated to the
encrypted key $\phi_{clsD}$ is:

$\footnotesize clsD=[\text{{AES-256-GCM}},null,null,FileProtectionNone]$

We represent the fact that the key is directly bound to the TEE and that no
additional ciphertext is required to decrypt this key (aside from the hardware
key of the SEP) by setting both the wrapping key value and the user
contribution, $authToken$, to null.

Figure 1: Boot, Unlock and File Decryption stages on Android (left) and iOS
(right) platforms are depicted here. Note that the process starts in the top
right corner in each diagram. In Android a user space algorithm loads the keys
from the system partition and starts the interaction with the secure enclave.
In IOS the process is started when the kernel loads the wrapped $\phi_{clsD}$
key from a kernel partition. The other keys are subsequently retrieved from
the user partition.

_$ClassC$ policy._ This is the default encryption policy for system and user
apps and user data. Like the $CE_{u}$ class in Android, this class key is made
available after first authentication, and not evicted when locking the device.
The key is protected by $k_{clsD}$ and requires an authentication token
consisting of a password derived key referred to as $k_{master\\_key}$ [2].
Using our syntax we describe the policy associated to a ClassC key
$\phi_{clsC}$ as:

$\footnotesize clsC=[\text{{AES-256-GCM}},\phi_{clsD},k_{master\\_key},\\\
FileProtectionCompeteUtilFirstUserAuthentication]$

_$ClassB$ policy._ This policy facilitates the ability to write encrypted data
when the device is locked, whilst at the same time prevent reading/access of
the same data using public key cryptography. This functionality is useful, for
example, when an e-mail attachment is downloading in the background [2]. In
order to use our syntax to describe this policy we have to split it into two
parts, the public key and private key parts. The public key of the policy is
made available once the device has booted (immediately after the ClassD key
$k_{clsD}$ as it is encrypted with it). The private key part, however, is only
released after first authentication, together with the ClassC key. Therefore
the two policies for describing the ClassB policy are:

$\footnotesize clsB_{pub}=[\text{{AES-256-GCM}},\phi_{clsD},null,\\\
FileProtectionCompleteUnlessOpen]$ $\footnotesize
clsB_{priv}=[\text{{AES-256-GCM}},\phi_{clsD},k_{master\\_key},\\\
FileProtectionCompleteUnlessOpen]$

We again capture the user contribution requirement in the decryption of the
ClassB private key part by setting the $authToken$ parameter.

_$ClassA$ policy._ The final policy is used in scenarios where data needs to
be protected at all times except when the device is unlocked. This
functionality is achieved non-cryptographically by wiping the ClassA keys from
memory 10 seconds after a device is locked. In iOS this is considered the
strongest level of protection [2]. Note that from a cryptographic point of
view, this policy provides the same key protection as the ClassC policy and
the private key of the ClassB policy. The functional differences333A ClassA
key will be cleared by the SEP OS 10s after the device is locked. A ClassC is
only cleared when the device is powered off. This means that the $authToken$
key is used multiple times in the case of the ClassA keys and only once in the
case of the ClassC keys. are captured by the usage parameter of the policy.
The policy is described as:

$\footnotesize clsA=[\text{{AES-256-GCM}},\phi_{clsD},k_{master\\_key},\\\
FileProtectionComplete]$

_Other keys._ In addition to the above-mentioned class keys, iOS uses three
more keys: (1) the key $k_{keybag}$ secures the keybag database containing the
wrapped $ClsA-C$ keys stored in the user partition, (2) the key $k_{metadata}$
encrypts the file system’s metadata information (e.g. file names), and (3) the
key $k_{effaceable}$ wraps both 1,2 and ClsD. The first two of these keys are
always stored and managed together with $k_{clsD}$. As such, for simplicity,
we refer to this group of keys ($k_{keybag}$, $k_{metadata}$, $k_{clsD}$) as
$k_{clsD}$ and make the distinction where necessary. Finally, $k_{effaceable}$
is outside the scope of this work as it provides no additional data
confidentiality, and is instead designed to aid with quick erase. Disposing of
this key renders all files cryptographically inaccessible.

##  4 Overview

When analysing key management for MFBE, first we want to distinguish between
the following two states of device: the provisioned state, when cryptographic
keys have been initialised on the device, and the not provisioned state, when
key material is missing from the device. A device will always be in the
provisioned state with the exception of right before being powered on for the
first time or right after it has been restored to default settings. While a
device in this state it will follow the first boot sequence. In every other
case the device will be in a provisioned state and will follow the regular
boot sequence.

As part of the regular boot sequence there are three core stages for both
Android and iOS: device unlock, first user-unlock, and regular file access
after first user-unlock. In Figure 1 the regular boot sequences for Android
and iOS are presented using the notation presented earlier.

The main difference between the first boot sequence and the regular boot
sequence is that the former includes a key generation stage which precedes all
the stages of the latter. The key generation algorithm is detailed in Section
5. However it is worth mentioning that while the iPhone’s SEP has a random
number generator that is used to directly generate the key material inside the
secure enclave, in Android the key material is generated in the non-trusted
environment and then exported to the enclave via system services that run in
the user space. In both systems, after the initial key generation the boot
process continues with the regular boot sequence.

1

Input: $k,w,pol$

Output: $\phi,\overline{pol}$

Constants: $\sigma=\\{\sigma\text{-}key,\sigma\text{-}ciph\\}$

2

3function  _$\mathsf{WrapKey}(k,w,pol)$_

4 $ciph\xleftarrow{}pol.cipher$

5 $\overline{pol}\xleftarrow{}pol$

6

/* Encrypt class keys $k$ with wrap key and policy cipher. */

7

8 /* DE class has no user token. */

_9_ _ _if  _pol.usage = DeviceDataAfterBoot_

_10_ __ or pol.usage = UserDataAfterBoot

_11_ __ /* CE class verifies the user token. */

_12_ __ or $(pol.usage=UserDataAfterAuth$

_13_ __ and VerifyToken(pol.authToken))

14 then

15 $\phi\xleftarrow{}ENC^{ciph}(k,w)$

16

/* Encrypt wrap key w and bind it to the policy. */

17
$\overline{pol}.wrapkey\xleftarrow{}ENC^{\sigma\text{-}ciph}(w,\sigma\text{-}key)$

18 return $\\{\phi,\overline{pol}\\}$

19 else

20 return $\bot$

21

Algorithm 1 $\mathsf{WrapKey}^{\sigma}$ in Android

1

Input: $k,w,pol$

Output: $\phi,\overline{pol}$

Constants: $\sigma=\\{\sigma\text{-}key,\sigma\text{-}ciph\\}$

2 function  _$\mathsf{WrapKey}(k,w,pol)$_

3 $ciph\xleftarrow{}pol.cipher$

4 $\overline{pol}\xleftarrow{}pol$

5

6 if  _$pol.usage=FileProtectionNone$_ then

/* ClassD i.e. FileProtectionNone */

7 $\phi^{\prime}\xleftarrow{}k$

8

9 else

10 if  _$pol.authToken=null$_ then

/* Encrypt class $\text{B}_{\text{pub}}$ key $k$ with wrap key $w$ and policy
cipher. */

11 $\phi^{\prime}\xleftarrow{}ENC^{ciph}(k,w)$

12

13 else

/* Encrypt class A, $\text{B}_{\text{prv}}$ and C keys $k$ with wrap key $w$,
policy cipher and user password derived key $k_{master\\_key}$. */

14 $k_{master\\_key}\xleftarrow{}pol.authToken$

15 $\phi^{\prime\prime}\xleftarrow{}ENC^{ciph}(k,k_{master\\_key})$

16 $\phi^{\prime}\xleftarrow{}ENC^{ciph}(\phi^{\prime\prime},w)$

17

/* Encrypt the wrapping key with the SEP’s key. */

18

19
$\overline{pol}.wrapkey\xleftarrow{}ENC^{\sigma\text{-}ciph}(w,\sigma\text{-}key)$

20

/* Encrypt wrapped keys $\phi^{\prime}$ with the hw. key. */

21

22
$\phi\xleftarrow{}ENC^{\sigma\text{-}ciph}(\phi^{\prime},\sigma\text{-}key)$

23 return $\\{\phi,\overline{pol}\\}$

Algorithm 2 $\mathsf{WrapKey}^{\sigma}$ in iOS

Device unlock is the first stage of the boot process during which the device
will decrypt the system partitions/files. There are some important differences
between Android and iOS in this stage. As mentioned before, in Android key
management is performed through services that run in the user space. A
consequence of this is that the boot process needs to reach the stage where
user space programs can be executed. This in turn means that the main system
partition has to be unencrypted so that important system components, such as
the kernel, can be loaded. Once the kernel and relevant key management
services are up and running, the main encrypted device keys,
$k_{DE_{\\{u,s\\}}}$ will be loaded from disk, decrypted inside the secure
enclave, exported back to the user space key management service and finally
loaded into the Android kernel memory space. Once the keys are available to
the kernel relevant locations on the data partition will be decrypted to allow
basic usage of the device (e.g. WiFi configuration details, phone and
messaging apps).

In iOS all encryption, decryption and key management is performed inside the
SEP. As such, in iOS the system partition can also be encrypted. In the
beginning stages of the boot process the iOS kernel will load the encrypted
class D key, $\phi_{clsD}$, which protects the whole filesystem, from the
system partition into the SEP to be decrypted and enabled for use. Once the
system and user partitions are decrypted by $k_{clsD}$ the ciphertexts for the
remaining class keys are loaded from the user partition into the SEP.

We consider the device boot stage complete when all the keys restricting
access to system related functionality have been loaded.

User unlock is the second stage of the boot process. During this stage the
device will decrypt and load the user specific keys. Access to these keys will
be conditioned on a user specific input, such as a password or biometric data,
which we refer to as Passcode. As detailed in Section 3.2, although the
passcode is handled differently between Android and iOS, the functionality
remains the same in the two platforms. Once the passcode is verified, the key
loading process follows a platform specific process similar to the one
described in the Device unlock stage.

File encryption/decryption unlock is the final stage of the boot process and
represents the regular use of the device. In both Android and iOS encryption
and decryption are performed transparently by algorithms running in the kernel
or SEP respectively. Android uses the Linux ext4 filesystem encryption and
decryption algorithm which we discuss in more detail in Section 6.1. We were
unable to find similar information related to the algorithms used in iOS.

##  5 Key management in mobile FBE schemes

In this section we give the generic algorithms needed to instantiate file-
based encryption in Android and iOS. We show that our models capture the
complete functionality of the actual implementations. In Fig. 1 we show the
interaction between the algorithms defined in this section, for the device
boot, unlock and file decryption stages.

_The $KGen$ algorithm._ We wanted to allow flexibility in our definition of
MobileFBE such that our syntax and proofs could easily adapt both to existing
schemes and to future schemes that aim to provide file-based encryption. To
this end we have defined the KGen as the probabilistic key generation
algorithm which is called whenever a random key is needed by any other
MobileFBE algorithm. This algorithm only takes as input a security parameter
and a key format. The output is a random sting that can be used as a key for
that specific format.

_The $\mathsf{WrapKey}$ algorithm._ This algorithm represents the first
MobileFBE specific algorithm. It uses the raw keys generated by $KGen$ and
protects them using one or more layers of encryption, depending on the type of
key, i.e. the key policy. The $\mathsf{WrapKey}$ takes as input the key to be
protected $k$, a wrapping key $w$, and a usage policy $pol$. The purpose of
the $\mathsf{WrapKey}$ algorithm is to cryptographically bind input values
$k$, and $pol$ to the trusted execution environment through the wrap key $w$.
We model the TEE through the constants
$\sigma=\\{\sigma\text{-}key,\sigma\text{-}ciph\\}$ representing the key
stored exclusively in the TEE and the cipher associated with that key,
respectively. An important aspect to notice is that, if no wrapping key is
given as input (i.e. $w$ is $null$) the input key $k$ will be protected by the
TEE (using the key $\sigma\text{-}key$ and the cipher $\sigma\text{-}ciph$).

We give two $\mathsf{WrapKey}$ algorithms, one for Android (Algorithm 1) and
one for iOS (Algorithm 2) to describe how the key wrapping is performed in
these systems. While these algorithms are very similar to one another we would
like to distinguish a few differences between them.

Android. Due to the hardware constraints imposed on devices that run Android
(i.e. very limited memory available exclusively to the TEE) on this platform
we distinguish two main types of keys: wrap keys and policy-based encryption
keys. As previously stated, in Android each policy-based encryption key $k$ is
protected by a hardware-backed wrapping key. However, because of the limited
storage available in the TEE these wrapping keys are stored outside the TEE,
encrypted with the key $\sigma\text{-}key$. In Algorithm 1 we model these
wrapping keys as part of the policy. The hardware-backing operation is shown
on line 11.

Another important implementation decision in Android is that the
$\mathsf{WrapKey}$ algorithm which protects device encryption keys (e.g.
$DeviceDataAfterBoot$ policy) is identical to the one which protects
credential encryption keys (e.g. $UserDataAfterAuth$ policy). The only
difference between the two being that the $UserDataAfterAuth$ policy requires
a valid authentication token before the wrapping (or unwrapping) is performed
as shown on line 9.

As such, for a wrapping key $w$ and a encryption key $k$, Algorithm 1 works as
follows. First the wrapping cipher is retrieved from the policy (line 2). Then
the policy is checked for usage (lines 5-8). If the $pol.usage$ field contains
a supported key usage policy then the encryption key $k$ is then encrypted
with $w$ using the cipher $ciph$ specified in the policy (as shown on line
11). Finally, the wrap key is encrypted inside the TEE and added to the
policy, thus binding key $k$ to the TEE through the policy pol, which now
contains the ciphertext of the wrapped key (line 12).

iOS. The $\mathsf{WrapKey}$ algorithm for iOS is presented in Algorithm 2.
This algorithm is similar in functionality to the Android WrapKey. However,
iOS does not use wrapping keys, instead this functionality is achieved using
multi-layered encryption as follows.

Currently, iOS distinguishes four policies for its policy-based encryption
keys: ClassA, ClassB, ClassC, ClassD. Each policy has an associated encryption
key. These keys are used both for wrapping other, more secure policy keys, as
well as providing the file based encryption functionality under the current
policy. The keys can be grouped into three security levels based on the number
of encryption layers used to wrap them.

Similarly to Android, iOS has a device unique key and cipher $\sigma$
available only to the TEE. The outer-most encryption layer uses this key to
protect all the iOS keys (Algorithm 2, line 3) and bind them to the secure
hardware element.

The encryption key for the ClassD policy, $k_{clsD}$ is the least-protected
key in iOS, being encrypted only with the TEE stored, device key
$\sigma\text{-}key$. The $k_{clsD}$ key is used both for file encryption to
provide the iOS defined FileProtectionNone security level as well as for
wrapping other policy keys. As such ClassD encrypts all other policy keys in
iOS (Algorithm 2, line 5).

The public key for the ClassB policy, $k_{clsB_{pub}}$ is the next least-
protected key, being encrypted with $k_{clsD}$ and $\sigma\text{-}key$. This
key is only used for file encryption, to provide write only capability to apps
under the FileProtectionCompeteUnlessOpen security policy usage (Algorithm 2,
lines 8).

Finally, keys used by ClassA and ClassC policies ($k_{clsA}$ and $k_{clsC}$),
and the private key of the ClassB policy ($k_{clsB_{prv}}$) are protected with
three layers of encryption. In addition to the $k_{clsD}$ and
$\sigma\text{-}key$ outer layers, a third inner encryption layer is provided
using a user authentication PIN/password/biometric derived key,
$k_{master\\_key}$. This use of this key effectively ensures that $k_{clsA}$,
$k_{clsC}$ and $k_{clsB_{prv}}$ cannot be accessed unless the user is able to
successfully authenticate and produce the user authentication derived key (2,
lines 11-12). In order to more accurately compare the Android and iOS
algorithms we are modelling $k_{master\\_key}$ as an authentication token
using our policy syntax.

_The $\mathsf{UnwrapKey}$ algorithm._ $\mathsf{UnwrapKey}$ performs the
opposite operation to that of $\mathsf{WrapKey}$. That is, given a wrapped key
$\sigma$ and the policy object associated with that key $\overline{pol}$, then
return the decrypted class key $k$ (for installation into the file manager’s
keyring). All platforms and class keys that we consider are hardware bound,
hence the algorithm also requires access to the secure hardware (TEE or
enclave).

A key element of $\mathsf{UnwrapKey}$ is to verify the context within which it
is executed. This is to ensure that keys cannot be arbitrarily unwrapped
without concern for the state of the device. The policies for each platform
state their usage scenarios, and these are checked when executing
$\mathsf{UnwrapKey}$. In general, the stricter policies require valid
$authTokens$ (see section 3.2) to successfully unwrap the class key. As
before, we will now differentiate the two implementations of
$\mathsf{UnwrapKey}$ on each considered platform.

Android. In Android, each policy contains it’s own hardware protected wrapping
key. In Algorithm 3, we can see that this is decrypted by the TEE on line 3.
If the DE policies are being initiated, then this wrap key is then directly
used to decrypt the class key (line 9). Otherwise, when the more secure CE
policy is in use, the system requires a successful generation and verification
of the $authToken$ to proceed (line 7). Although authTokens are not
cryptographically used to protect the CE key, the TEE will not proceed with
the key decryption until a $authToken$ has been provided and verified.

iOS. Unwrapping keys in iOS consists of iteratively removing layers of
encryption. Each call to the function will first begin by removing the
hardware encryption layer, which all supported class keys are protected with
(line 3). As described in the previous section, each class key has varying
encryption layers and dependencies. The logic which defines how to decrypt
each key is defined in lines 4-13. Notably, to remove the final encryption
layer on the most secure class keys (A, Bprv, and C), the iOS version of a
valid authToken is required (i.e. the $k_{master\\_key}$). In contrast to
Android, this $k_{master\\_key}$ is directly used to encrypt the keys
belonging to the relevant classes.

_The $\mathsf{ProvisionKey}$ & $\mathsf{EvictKey}$ algorithms (Appendix 0..3
alg. 10 & 11)._ In Android and iOS keys are not accessed directly, but through
data structures called key handles that are similar to memory pointers. Use of
these handles allows the actual key plaintext to be stored securely, for
example in the TEE’s memory while, at the same time, enabling programs running
outside of this context, (e.g. user-land programs), to use the keys for
cryptographic operations, without actually having access to the key itself. We
capture this functionality through the $\mathsf{ProvisionKey}$ algorithm. This
algorithm simply takes as input a plaintext key and returns a key handle $kid$
which can safely be exported and used outside the hardware context which
performs the actual cryptographic operations. The $\mathsf{ProvisionKey}$
algorithm plays an important role in the security of the scheme, as running it
in the wrong context could lead to the key plaintext being stored in an unsafe
memory location or leaked.

The $\mathsf{EvictKey}$ algorithm is the algorithm used to clear the plaintext
of a key from memory using the key’s handle, $kid$. Key should be an operation
that can be safely run in any context as it does not have direct access to any
cartographic key material.

1

Input: $\phi,\overline{pol}$

Output: $k$

Constants: $\sigma=\\{\sigma\text{-}key,\sigma\text{-}ciph\\}$

2

3function  _$UnwrapKey(\phi,\overline{pol})$_

4 $ciph\xleftarrow{}\overline{pol}.cipher$

5
$w\xleftarrow{}DEC^{\sigma\text{-}ciph}(\overline{pol}.wrapkey,\sigma\text{-}key)$

6

_7_ _ _if  _pol.usage = DeviceDataAfterBoot_

_8_ __ or pol.usage = UserDataAfterBoot

_9_ __ or $(pol.usage=UserDataAfterAuth$

_10_ __ and VerifyToken(pol.authToken))

11 then

12 $k\xleftarrow{}DEC^{ciph}(\phi,w)$

13 return $k$

14 else

15 return $\bot$

16

Algorithm 3 UnwrapKeyσ in Android

##  6 File Content Encryption in Mobile FBE Schemes

In this section we propose a formal description of the file encryption scheme
used by the EXT4 filesystem as it has been implemented in Android and *NIX
systems. We have not been able to access the source code of the software
produced by Apple (i.e. all Apple software is closed source). However, we
speculate that the iOS implementation of FBE is conceptually similar to the
EXT4 implementation.

###  6.1 Android EXT 4 Case Study

The EXT4 encryption is a FBE scheme originally developed by Google [17] for
use with the Android 7.0 and higher. It became part of the mainline kernel in
version 4.0 under the name of Filesystem-level encryption (fscrypt) and has
suffered some adaptations. Google continues to maintains the corresponding
User space tool (also named fscrypt) for use with the kernel API discussed in
the following.444https://github.com/google/fscrypt

1

Input: $\phi,\overline{pol}$

Output: $k$

Constants: $\sigma=\\{\sigma\text{-}key,\sigma\text{-}ciph\\}$

2 function  _$UnwrapKey(\phi,\overline{pol})$_

3 $ciph\xleftarrow{}\overline{pol}.cipher$

/* Remove the hardware encryption layer from $\phi$. */

4 $k^{\prime}\xleftarrow{}DEC^{\sigma\text{-}ciph}(\phi,\sigma\text{-}key)$

5

6 if  _$pol.usage=FileProtectionNone$_ then

/* FileProtectionNone i.e. ClassD */

7

8 $k\xleftarrow{}k^{\prime}$

9

10 else

/* Decrypt wrap key $w$. */

11
$w\xleftarrow{}DEC^{\sigma\text{-}ciph}(\overline{pol}.wrapkey,\sigma\text{-}key)$

12

/* Decrypt class $\text{B}_{\text{pub}}$ and the 1st layer for class A,
$\text{B}_{\text{prv}}$ or class C keys with wrap key $w$ and policy cipher.
*/

13 $k^{\prime\prime}\xleftarrow{}DEC^{ciph}(k^{\prime},w)$

14

15 if  _$pol.authToken=null$_ then

16 $k\xleftarrow{}k^{\prime\prime}$

17 else

/* Decrypt class A, $\text{B}_{\text{prv}}$ or C keys $k$ with user key. */

18

19 $k_{master\\_key}\xleftarrow{}pol.authToken$

20 $k\xleftarrow{}DEC^{ciph}(k^{\prime\prime},k_{master\\_key})$

21

22

23

24 return $k$

Algorithm 4 UnwrapKeyσ in iOS

There are currently three main modes in which fscrypt can function on Android.
First is the original scheme developed by Google for Android 7.0. This scheme
is currently summarised under the v1 policy in the official documentation [21]
and suffered from several limitations as follows. Even though per-file
encryption keys were derived from a master key (such as $k_{CE}$),
compromising one of these could result in compromising the master key from
which the per-file key was derived from. This is mainly due to the odd use of
a publicly known random value, $n$ as the key input to the AES cipher used for
key derivation. This is captured in Algorithm 6, line 3 and is described in
more detail in the next section. Additional limitations to v1 were also the
lack of verification for the master key usage which would allow malicious
users to gain read only access to other user’s encrypted files, and also there
were difficulties in removing encryption keys from memory in order to limit
access to protected files [21]. Addressing these issues has resulted in an
enhanced fscrypt and a new key derivation function, summarised under the v2
policy.

Finally, starting with Android 10 fscrypt started supporting a new cipher,
Adiantum, developed by Google [13] and aimed at
performance.555https://security.googleblog.com/2019/02/introducing-adiantum-
encryption-for.html With the addition of this new cipher a new mode of
operation for fscrypt was also added, Adiantum.Direct_Key which no longer uses
a KDF. The Adiantum cipher however can also be used with v1 and v2 policies.

In the following we propose several algorithms which summarise and simplify
the way in which fscrypt is implemented in Android (and the Linux kernel).
These algorithms also allow us to directly compare the security and features
of the various modes supported currently and in the future by fscrypt.

The EXT4 filesystem uses the notion of nodes to generically describe its
components: files, directories and symbolic links. In our pseudo-code we have
used the same notation to describe the sequence of operation needed to perform
FBE operations. To simplify notation, we define an EXT4 node as a tuple
$node=(name,\allowbreak meta,\allowbreak type,\allowbreak content,\allowbreak
children)$ where:

  * –

$node.name$: is the file or directory name of the node.

  * –

$node.meta$: is a storage container associated with the node different from
the main content of the file. It stores metadata information such as
permissions, data access information, etc., but also the xattr attribute which
stores the unique cryptographic nonce of the node.

  * –

$node.type$: represents the type of the node, i.e. file or directory.

  * –

$node.content$: in case $node.type$ is a file the content represents the main
storage container for the node. This mainly refers data stored inside files.

  * –

$node.children$: in case $node.type$ is a directory the $node.children$ will
be a set of all the $node.names$ contained inside that node, i.e. the names of
the file and sub-directories contained in the specified node.

Input: $\textit{f}node,kid,mode$

Output: $enode$

1 function  _$\mathsf{\mathsf{Encrypt}}(\textit{f}node,kid)$_

2 $k_{m}\xleftarrow{}{}GetKeyFromKernelKeyring(kid)$

3 if  _$k$_ then

4 $n\xleftarrow{}{\textit{f}}node.meta$

5 if  _$n=null$_ then

/* New fnode. */

6 $n\xleftarrow{R}\\{0,1\\}^{128}$

7

8 $enode.meta\xleftarrow{}n$

9

/* Filename/metadata is protected by directory sec context */

10 if  _$\textit{f}node.type=directory$_ then

11 $k_{e}\xleftarrow{}KDF(k_{m},n,mode)$

12
$enode.children\xleftarrow{}ENC^{\textit{f}}s\mbox{\\_}ciph(\textit{f}node.children,k_{e})$

13

14

/* File contents is protected by file sec context */

15 else if  _$\textit{f}node.type=file$_ then

16 $k_{e}\xleftarrow{}KDF(k_{m},n,mode)$

17
$enode.content\xleftarrow{}ENC^{\textit{f}}s\mbox{\\_}ciph(\textit{f}node.content,k_{e})$

18

19 return $enode$

20 else

21 return $\bot$

22

Algorithm 5 File encryption in EXT4 filesystems (Android & *NIX systems)

Additionally, to facilitate comparison between the supported FBE modes of
operation we also define the encryption keys as $k=(mode,\allowbreak val)$
where $k.mode$ represents the fscrypt mode in which the key is used and
$k.val$ is the actual binary value of the key.

In order to perform encrypt (or decrypt) operations a master key is required.
There can be any number of master keys in use simultaneously on a system. In
Android these keys are generated and made available to the kernel as described
in Section 5. In regular *NIX systems these keys need to be made available to
the kernel by the User space [21]. Once a key is loaded into the kernel a
unique key id, $kid$, is generated for use in User space. All encrypt and
decrypt operations will be managed transparently by the kernel, and keys will
be specified through their ids.

EXT4 encryption does not use the master keys directly, instead, it uses
individual keys for each $node.name$ and each $node.content$. These keys are
derived from the master key based on the fscrypt policy used and the 128bit
unique random nonces associated with each node. The policy will define the
ciphers used for encryption (and decryption), including the generation and use
of IV values, and the key derivation function (KDF) to be used for generating
individual per-file keys.

All policies employ block-chaining modes for disk encryption when encrypting
the $node.content$ and thus provide similar level of security. These modes
make use of hardware dependent values such as the logical block number (lbn)
of the storage device to generate unique IV values. This however is not the
case when encrypting $node.names$, and thus the policy plays a more
significant role in how much detail is revealed about these.

Input: $k,n,mode$

Output: $k_{e}$

1 function  _$\mathsf{KDF}(k,n,mode)$_

2 if  _$mode=\mathsf{v_{1}}$_ then

/* Original mode */

3 ${k_{e}}.\mathsf{val}\xleftarrow{}AES\text{-}128\text{-}ECB(k,n)$

4

5 else if  _$mode=\mathsf{Adiantum.DIRECT\\_KEY}$_ then

6 ${k_{e}}.\mathsf{val}\xleftarrow{}k$

7

8 else if  _$mode=\mathsf{IV\\_INO\\_LBLK\\_64}$_ then

9
${k_{e}}.\mathsf{val}\xleftarrow{}\mathsf{HKDF\text{-}SHA512}(k,mode\|\mathsf{<uuid>})$666UUID:
Universally Unique Identifier used to identify disk partitions.

10

11 else

/* Default: per-file keys */

12 $cb\xleftarrow{R}\\{0,1\\}^{8}$

13
${k_{e}}.\mathsf{val}\xleftarrow{}\mathsf{HKDF\text{-}SHA512}(k,\mathsf{"fscrypt"}\|cb\|n)$777Literal
string ”fscrypt” concatenated with a context byte ($cb$) and $n$.

14

15 ${k_{e}}.mode\xleftarrow{}mode$

16 return $k_{e}$

Algorithm 6 Key derivation (Android & *NIX systems)

1

Input: $content,k$

Output: $econtent$

2 function  _$ENC^{\textit{f}s\mbox{\\_}ciph}(content,k)$_

3 for  _$cblock\in content$_ do

4 $\mathsf{iv}\xleftarrow{}\mathsf{GetIV}(cblock,k.mode)$

5 $eblock\xleftarrow{}CIPHER(cblock,k.\mathsf{val},\mathsf{iv})$

6 $econtent\xleftarrow{}econtent\|eblock$

7

8

Algorithm 7 Node content encrypt (Android & *NIX systems)

1) Fscrypt key derivation methods

The v1 policy. In this policy the individual per-file keys are derived from a
master key using a KDF based on AES-256-ECB by simply encrypting the master
key with the node’s random 128bit nonce as shown in Algorithm 6 line 3. This
method was chosen to reduce the size of the cryptographic metadata stored on
disk. It is noted however by the authors that this requires the derived key to
be ”equally as hard to compromise” as the original master key and is currently
considered to be a security limitation [21].

The v2 policy. This policy replaces the AES-256-ECB based KDF with a HKDF-
SHA512 for generating per-file keys. In addition to being irreversible, the
new derivation method also takes as input an application-specific string in
addition to the master key. These modification successfully mitigate the
problems related to master key recovery from per-file encryption keys as well
as key reuse between applications (Algorithm 6 lines 9-10). The v2 policy also
supports generating keys for use with encryption hardware compliant with the
UFS or eMMC standards, under the IV_INO_LBLK_64 sub-policy (Algorithm 6 line
6-7). This sub-policy also enforces a specific form for the IV as detailed
below.

Adiantum.DIRECT_KEY. This is not a policy in itself rather the absence of one.
In Adiantum.DIRECT_KEY the master key is directly used to encrypt $node.name$
and $node.content$ for all the nodes in the file system. This mode however is
restricted to the Adiantum cipher as it relies on the cipher’s ability to make
use long IVs as described below.

2) Encryption

Currently, Fscrypt supports AES-256-XTS, AES-128-CBC and Adiantum for
$node.contents$ encryption and AES-256-CTS-CBC, AES-128-CTS-CBC and Adiantum
for $node.name$ encryption. Each of these ciphers will use different methods
for generating valid IV’s based on the key derivation method, and whether they
are used for encrypting $node.names$ or $node.content$.

Node’s content encryption. In the default configuration for encrypting the
$\allowbreak node.content$ under both v1 and v2 key derivation methods the IV
is initialised with the logical block number of the block residing on the
storage device. This IV can be used directly with AES-XTS and Adiantum (in non
DIRECT_KEY configuration). AES-CBC requires a random IV to achieve the desired
security properties, as such this is achieved by encrypting the lbs with a
SHA256 hash of the per-file encryption key (see Algorithm 8, lines 7-9).

An exception also exists for the IV_INO_LBLK_64 sub-policy which describes the
generation of a 64bit IV from a 32bit truncated lbn and another 32bits limited
value representing the nodes innode number 888a uniquely existing number for
all the nodes on the EXT4 partition (Algorithm 8, lines 10-11). Under
Adiantum.DIRECT_KEY the IV is obtained by concatenating the full 64bit lbn
with the node’s random nonce as shown in Algorithm 8, lines 12-13.

Node’s name encryption. Like most filesystems EXT4 is structured in a tree-
like format. This enables specific filesystem functionality, such as managing
permissions, browsing contents, searching, deleting, etc., to be efficient.
The fscrypt has been implemented such that encrypted EXT4 filesystems will
continue to have all the functionality of non-encrypted EXT4 filesystems.

As such, to support some of these operations, node names are encrypted using
keys associated to the parent node, e.g. the name of a file is encrypted with
the key corresponding to the directory where is it stored. However, node names
(and other metadata associated with nodes) are stored separately from the
node’s contents, and device blocks are often shared when storing, thus lbn
values cannot be used as IV values. Similarly, block chaining modes that rely
on the lbn XTS are also unsuitable.

In order to address this fscrypt restricts the ciphers and modes to AES-CTS-
CBC and Adiantum when encrypting node names. In the default configuration an
all-zero IV is used (Algorithm 8, line 6). Given that the key is also shared
between all children inside a node this results in encryption deterministic
which leaks information about the names. This limitation is mitigated when
Adiantum.DIRECT_KEY and IV_INO_LBLK_64 policies are used as the IV in these
cases are less dependent on the lbn. We detail this in Algorithm 8.

The cryptographic algorithms used for the encryption and decryption of file
names in a directory (i.e. node name) are very similar to the ones used for
encrypting blocks of content in a file (i.e. node contents). We model both in
Algorithms 7 and 12 respectively, with the added clarification that in the
former case the iteration is done on $node.names$ whereas in the latter on
$\textit{f}sblocks$.

Input: $\textit{f}sblock,mode$

Output: $\mathsf{iv}$

1 function  _$\mathsf{GetIV}(\textit{f}sblock,mode)$_

2 $\textit{f}node\xleftarrow{}GetInodeOf(\textit{f}sblock)$

3

4 if  _$\textit{f}node.type=file$_ then

5 $lbn\xleftarrow{}\textit{f}sblock.lbn$

6

7 else

/* Directory */

8 $lbn\xleftarrow{}\\{0\\}^{128}$

9

10

11

12 if  _$mode=\mathsf{AES\text{-}128\text{-}CBC}$_ then

13 $k_{\mathsf{iv}}\xleftarrow{}\mathsf{SHA256}(k)$

14
$\mathsf{iv}\xleftarrow{}\mathsf{AES\text{-}256\text{-}ECB}(lbn,k_{\mathsf{iv}})$

15

16 else if  _$mode=\mathsf{IV\\_INO\\_LBLK\\_64}$_ then

17
$\mathsf{iv}\xleftarrow{}lbn_{len=32b}\|\textit{f}node.InodeNumber_{len=32}$

18

19 else if  _$mode=\mathsf{Adiantum.DIRECT\\_KEY}$_ then

20 $\mathsf{iv}\xleftarrow{}lbn_{len=64b}\|\textit{f}node.meta_{len=128b}$

21

22 else

/* Default mode */

23 $\mathsf{iv}\xleftarrow{}lbn$

24 return $\mathsf{iv}$

Algorithm 8 Get IV (Android & *NIX systems)

##  7 Security analysis models

In this section we consider several adversarial models that affect the
security of FBE in mobile devices

$Exp_{\mathcal{A}}^{\mathsf{MFBE},b}(\lambda)$
$\sigma\xleftarrow{R}\\{0,1\\}^{*}$
$K:\\{(k,kid)|(\forall(k^{\prime},kid^{\prime})\in K)[kid\neq
kid^{\prime}]\\}$ $K\xleftarrow{}\emptyset$
$(state,\textit{f}node_{0},\textit{f}node_{1},kid^{\star})\xleftarrow{}\mathcal{A}_{1}^{\mathcal{O}^{wrap},\mathcal{O}^{unwrap},\mathcal{O}^{reveal},\mathcal{O}^{enc}}(1^{\lambda})$
$enode_{b}\xleftarrow{}\mathsf{Encrypt}(kid^{\star},\textit{f}node_{b})$
$b^{\prime}\xleftarrow{}\mathcal{A}_{2}^{\mathcal{O}^{wrap},\mathcal{O}^{unwrap},\mathcal{O}^{reveal},\mathcal{O}^{enc},\mathcal{O}^{dec}}(state,enode_{b})$
$\mathbf{return}~{}b^{\prime}$ Oracle $\mathcal{O}^{wrap}(pol)$
$k,w\xleftarrow{}\mathsf{KGen}(1^{\lambda})$
$(\phi,\overline{pol})\xleftarrow{}\mathsf{WrapKey}^{\sigma}(k,w,pol)$
$\mathbf{return}~{}(\phi,\overline{pol})$ Oracle
$\mathcal{O}^{unwrap}(\phi,\overline{pol})$
$k\xleftarrow{}\mathsf{UnwrapKey}^{\sigma}(\phi,\overline{pol})$
$\mathbf{if}~{}k~{}\mathbf{then:}$
$kid\xleftarrow{}\mathsf{ProvisionKey}(k,\overline{pol})$
$K\xleftarrow{}K\cup\\{(k,kid)\\}$ $\mathbf{return}~{}kid$ $\mathbf{else:}$
$\mathbf{return}~{}\bot$ Oracle $\mathcal{O}^{enc}(kid,{\textit{f}}node)$
$\mathbf{if}~{}(\cdot,kid)\in K~{}\mathbf{then:}$
$enode\xleftarrow{}\mathsf{Encrypt}(kid,{\textit{f}}node)$
$\mathbf{return}~{}enode$ $\mathbf{else:}$ $\mathbf{return}~{}\bot$ Oracle
$\mathcal{O}^{dec}(kid,enode)$ $\mathbf{if}~{}(\cdot,kid)\in
K~{}\mathbf{then:}$ $\textit{f}node\xleftarrow{}\mathsf{Decrypt}(kid,enode)$
$\mathbf{return}~{}\textit{f}node$ $\mathbf{else:}$ $\mathbf{return}~{}\bot$
Oracle $\mathcal{O}^{reveal}(kid)$ $\mathbf{if}~{}(k,kid)\in
K~{}\mathbf{then:}$ $\mathbf{return}~{}k$ $\mathbf{else:}$
$\mathbf{return}~{}\bot$

Figure 2: MobileFBE security experiment.

_Encryption model._ This adversarial model focuses on attacks against the
confidentiality of files contents and filenames that are part of the underling
filesystem. This adversarial model does not consider the confidentiality of
the non-filename metadata such as number of files, timestamps and permissions.
This attack also does not consider timing attacks and access frequency attacks
that might reveal information about how the system is used.

_Key security model._ This adversarial model focuses on attacks related to key
generation and key recovery.

_Permissions model._ This adversarial model focuses on attacks that break the
cryptographic access controls as enforced by the keys.

###### Definition 2

The security of a MobileFBE encryption scheme is defined through a security
experiment as follows (Figure 2). Let
$\mathsf{MFBE}{}=\allowbreak(\allowbreak\mathsf{KGen},\allowbreak\mathsf{WrapKey},\allowbreak\mathsf{UnwrapKey},\allowbreak\mathsf{ProvisionKey},\allowbreak\mathsf{EvictKey},\allowbreak\mathsf{Encrypt},\allowbreak\mathsf{Decrypt})$
be a mobile encryption scheme with a security parameter $\lambda$ and a two
stage adversary $\mathcal{A}=(\mathcal{A}_{1},\mathcal{A}_{2})$. We consider
$Exp_{\mathcal{A}}^{\mathsf{MFBE},b}(\lambda)$ a probabilistic experiment
defined in terms of a game played between an adversary $\mathcal{A}$ and a
challenger $\mathcal{C}$, consisting of:

  1. 1.

Setup. $\mathcal{C}$ initialises the hardware key $\sigma$ with a random
string and creates an empty set $K$ which keeps track of associations between
keys $k$ and their unique $kid$ handles as $(k,kid)$ pairs.

  2. 2.

Query. Adversary $\mathcal{A}_{1}$ queries oracles $\mathcal{O}^{wrap}$,
$\mathcal{O}^{unwrap}$, and $\mathcal{O}^{reveal}$.

  3. 3.

Challenge. The challenger receives from the adversary $\mathcal{A}_{1}$ a
$kid^{\star}$, and two file nodes $\textit{f}node_{0}$ and
$\textit{f}node_{1}$ , such that $\mathcal{O}^{reveal(kid^{\star})}$ has never
been queried. $\mathcal{C}$ runs
$enode^{\star}\leftarrow\mathsf{Encrypt}(kid^{\star},\textit{f}node_{b})$ to
encrypt $\textit{f}node_{b}$, and returns $enode^{\star}$.

  4. 4.

Guess. $\mathcal{A}_{2}$ outputs $b^{\prime}\in\\{0,1\\}$. In addition to the
oracles $\mathcal{O}^{wrap},\mathcal{O}^{unwrap},\mathcal{O}^{enc}$,
$\mathcal{A}_{2}$ is given access to the oracle $\mathcal{O}^{reveal}$ but
cannot query $\mathcal{O}^{reveal(kid^{\star})}$, and the oracle
$\mathcal{O}^{dec}$ but cannot query $\mathcal{O}^{dec(kid^{\star},enode)}$
such that $enode$ is either the challenge ciphertext or is produced by the
oracle $\mathcal{O}^{enc(kid^{\star},\cdot)}$. The output of the experiment is
$b^{\prime}$.

We capture the adversary’s abilities using formal definitions of oracles in
Figure 2. Below we provide the intuition for these oracles.

$\mathcal{O}^{wrap}$:

Allows the adversary to create $\mathsf{MFBE}{}$ keys. Receives as input an
policy $pol$. For this policy the oracle generates a key $k$ and a wrapping
key $w$ using the key generation algorithm $KGen(1^{\lambda})$. Then the key
$k$ is encrypted with the wrapping key as specified in the $WrapKey$
algorithm. Inside $WrapKey$ $w$ is also encrypted with the hardware key
$\sigma$ and is returned as part of the hardware-bound policy
$\overline{pol}$. The oracle maintains a state of all the generated keys k
using the set $S$. Finally, the ciphertext of $k$, $\phi$ is returned together
with its bounding policy $\overline{pol}$.

$\mathcal{O}^{unwrap}$:

Allows the adversary to instantiate $\mathsf{MFBE}{}$ keys generated under a
specific policy. Receives as input an encrypted key $\phi$ and its associated
policy $\overline{pol}$. Recovers the key using the wrap key from the policy
and authenticated is using the key set $S$. If the key is valid a key handle
$kid$ is returned ($\bot$ otherwise). The links between key ids and keys are
maintained using the key map $K$.

$\mathcal{O}^{enc}$:

Allows the adversary to encrypt a file node $\textit{f}node$ using a key id
$kid$. The oracle returns the encrypted file node $enode$ if the encryption
was successful and $\bot$ otherwise.

$\mathcal{O}^{dec}$:

Allows the adversary to decrypt a previously encrypted $enode$ using a key id
$kid$. The oracle returns the decrypted file node $\textit{f}node$ if the
decryption was successful and $\bot$ otherwise.

$\mathcal{O}^{reveal}$:

Allows the adversary to obtain the key associated to a valid handle $kid$.

######  Definition 3 (Security of $\mathsf{MFBE}{}$)

A mobile file based encryption scheme $MobileFBE{}$ is secure if the advantage
defined as:

$Adv_{\mathcal{A}}^{\mathsf{MFBE}}(\lambda)=\Big{\lvert}\mathsf{Pr}\Big{[}{\mathrm{Exp}}_{\mathcal{A}}^{\mathsf{MFBE},1}(\lambda)=1\Big{]}-\mathsf{Pr}\Big{[}{\mathrm{Exp}}_{\mathcal{A}}^{\mathsf{MFBE},0}(\lambda)=1\Big{]}\Big{\rvert}$

is negligible in $\lambda$ for any polynomial based two stage adversary
$\mathcal{A}=(\mathcal{A}_{1},\mathcal{A}_{2})$.

Below we shall analyse the security of the Android implementation given in
Algorithm 1, 3, 5, 9, with the following simplification and generalisation:

  * •

In the file encryption algorithm in Algorithm 5, the file name is encrypted
with a constant iv which makes the encryption deterministic and breaks the
$\mathsf{MFBE}$ security definition. However, as mentioned before, this is
used for maintaining equality relationship between encrypted and non-encrypted
nodes. Therefore, in our security model, we ignore the file name encryption
part, i.e., line 7-13 in Algorithm 5 and line 5-8 in Algorithm 9, and only
model the file content encryption. Formally,

    * –

We model the key derivation function, i.e., $ENC^{AES-128-ECB}(k,\cdot)$ as a
pseudorandom function (PRF) $F_{k}(\cdot)$;

    * –

We write $ENC^{file\texttt{-}ciph}$ and $DEC^{file\texttt{-}ciph}$ for the
cipher used for encrypting/decrypting the file content.

    * –

We simplify the file node structure and only consider two fields, i.e.,
$node=(meta,content)$. We require that the challenge file nodes
${\textit{f}}node_{0}$ and ${\textit{f}}node_{1}$ satisfy
${\textit{f}}node_{0}.meta={\textit{f}}node_{0}.\allowbreak meta=null$ and
$\left\lvert{{\textit{f}}node_{0}.\allowbreak
content}\right\rvert=\left\lvert{{\textit{f}}node_{1}.\allowbreak
content}\right\rvert$.

  * •

User authentication in $\mathsf{WrapKey}$ (Algorithm 1) and
$\mathsf{UnwrapKey}$ (Algorithm 3) is not relevant to the security. For
simplicity, in our security analysis we omit the user authentication part,
i.e., the if branch ”if $pol.usage=UserDataAfterAuth$…”.

  * •

We assume the cipher $ciph$ used for encrypting the class key
$ENC^{ciph}(k,w)$ is fixed. If we allow users to choose $ciph$, then we need
additional mechanism to guarantee each wrap key $w$ will only be used for a
certain type of cipher. This can be achieved by, for example, encrypting the
cipher type with the wrap key, i.e.,
$ENC^{\sigma\mbox{-}ciph}(w\|ciph,\sigma\mbox{-}key)$.

###### Theorem 7.1

The Android $\mathsf{MFBE}{}$ is secure if $ciph$ and $\sigma\text{-}ciph$ are
IND-CPA and INT-CTXT secure, $F$ is a family of pseudorandom functions, and
$file\text{-}ciph$ is IND-CCA secure. Formally, for any adversary
$\mathcal{A}$ that attacks $\mathsf{MFBE}$, runs in time at most $\tau$ and
makes at most $q_{w}$ queries to $\mathcal{O}^{wrap}$, there exist adversaries
$\mathcal{B}_{1},\dots,\mathcal{B}_{6}$ such that they run in time at most
$\tau$ and

$\displaystyle Adv$ ${}_{\mathcal{A}}^{\mathsf{MFBE}}\leq
2Adv_{\sigma\mbox{-}ciph,\mathcal{B}_{1}}^{CTXT}+2Adv_{\sigma\mbox{-}ciph,\mathcal{B}_{2}}^{CPA}+2q_{w}Adv_{ciph,\mathcal{B}_{3}}^{CTXT}$
$\displaystyle\quad+2q_{w}Adv_{ciph,\mathcal{B}_{4}}^{CPA}+2q_{w}Adv_{F,\mathcal{B}_{5}}^{PRF}+q_{w}Adv_{\textit{f}s\mbox{\\_}ciph,\mathcal{B}_{6}}^{CCA}$

See Appendix 0..1 for a proof.

_Cipher modes security._ In the following we briefly recall well-known
symmetric encryption schemes and their security properties:

  * •

AES-GCM [28]: The Galois/Counter Mode of Operation (GCM) is a widely deployed
authenticated encryption scheme, which is proven to be IND-CTXT and IND-CCA
secure [31]

  * •

AES-CBC: with random IV acting as a nonce achieves IND-CPA security [38,
Chapter 13]

  * •

Adiantum [13]: a tweakable, variable-input-length, super-pseudorandom
permutation that it is used as a fast length-preserving encryption scheme that
cannot achieve IND-CCA nor IND-CPA security

  * •

Well-known generic symmetric encryption modes that achieve IND-CTXT/CCA
security include [38]:

    * –

IND-CPA encryption + strong MAC (e.g., HMAC/CBC-MAC) $\rightarrow$ IND-CTXT
encryption

    * –

IND-CPA + IND-CTXT $\rightarrow$ IND-CCA encryption

##  8 Related Work

Prior to the adoption of File-based encryption (FBE), Full-Disk encryption
(FDE) technologies were the encryption method of choice for most desktops,
mobiles and other devices. FDE schemes have been extensively researched both
formally, and implementations thereof. See for example Rogaway [35] and Khati
et al. [24] for formal analyses, and [10] for practical implementation
analyses.

The original encrypting file system, Matt Blaze’s CFS [9], transparently
encrypted data passing through a user-level NFS daemon. A variation of CFS,
named Cryptfs, which leveraged virtual inodes, was presented in the late 90s
[43]. This was then extended by Halcrow in [22], which years later has now
been updated and adopted for use in Android as the EXT4 filesystem [21].

Early analysis of major mobile OS vendor encryption schemes started with [32],
[4], [3] on iOS. This works were followed by a framework for high-level
security analysis proposed in [41]. The authors subsequently presented case
studies on iOS [42] and Android [40]. Our work adopts some of the threat
models from these proposals, however we take things further by providing a
formal analysis. We also update the analysis of [40] with our consideration of
Androids FBE scheme, whereas before only the FDE scheme was analysed.

Related to works analysing the Android encryption schemes are those focusing
on secure key storage and management. Cooijmans et al [12] evaluate various
key storage solutions in Android. Sabt et al [36] carry out a cryptanalysis of
Android KeyStore and formally prove the encryption scheme does not provide
integrity, enabling forgery attacks. Implementation flaws discovered through
reverse engineering efforts include those of [8] and [23].

Due to the overhead in software based disk-encryption there has been a push
for hardware solutions in recent years [30, 27]. Meijer et al. [29] find many
critically flawed implementations of this in SSDs. They highlight the risk
posed by an OS that relies on third party encryption implementations, using
the example of Microsoft’s BitLocker. Apple’s software and hardware is tightly
coupled, and as such, this diversity of vendors and implementations is less of
a concern.

##  9 Conclusion

File-based encryption schemes have been developed independently by Apple for
their iOS mobile OS and by Google for Android. The initial Android proposition
was subsequently extended and added to mainline Linux kernel. However, given
that these schemes originate from commercial applications their security
properties have only been supported by high-level descriptions and anecdotal
evidence. In this work we are bridging this gap by rigorously proving the
industry claimed security properties for the analysed schemes. Furthermore,
through our proposed definitions and evaluation models we hope to enable the
security of future schemes to be more easily assessed.

## References

  * [1] Apple.  Answers to your questions about apple and security, 2016.  https://www.apple.com/customer-letter/answers/.
  * [2] Apple.  ios security guide, 2019.  https://www.apple.com/business/site/docs/iOS_Security_Guide.pdf.
  * [3] Jean-Baptiste Bédrune and Jean Sigwald.  iphone data protection in depth.  Vortrag von der HITB-SecConf, 2011.
  * [4] Andrey Belenko.  Overcoming ios data protection to re-enable iphone forensics.  Black Hat USA, 2011.
  * [5] Andrey Belenko.  ios forensics with open-source tools.  In Blackhat, 2014.
  * [6] Mihir Bellare, Anand Desai, Eron Jokipii, and Phillip Rogaway.  A concrete security treatment of symmetric encryption.  In Proceedings 38th Annual Symposium on Foundations of Computer Science, pages 394–403. IEEE, 1997.
  * [7] Mihir Bellare and Chanathip Namprempre.  Authenticated encryption: Relations among notions and analysis of the generic composition paradigm.  Journal of Cryptology, 21(4):469–491, 2008.
  * [8] G Beniamini.  Extracting qualcomm’s keymaster keys-breaking android full disk encryption, 2016.
  * [9] Matt Blaze.  A cryptographic file system for unix.  In Proceedings of the 1st ACM conference on Computer and communications security, pages 9–16. ACM, 1993.
  * [10] Omar Choudary, Felix Gröbert, and Joachim Metz.  Infiltrate the vault: Security analysis and decryption of lion full disk encryption.  IACR Cryptology ePrint Archive, 2012:374, 2012.
  * [11] CNN.  iphones and ipads need multi-user support now, 2018.  https://www.cnet.com/news/iphones-and-ipads-need-multi-user-support-now/.
  * [12] Tim Cooijmans, Joeri de Ruiter, and Erik Poll.  Analysis of secure key storage solutions on android.  In Proceedings of the 4th ACM Workshop on Security and Privacy in Smartphones & Mobile Devices, pages 11–20. ACM, 2014.
  * [13] Paul Crowley and Eric Biggers.  Adiantum: length-preserving encryption for entry-level processors.  IACR Trans. Symmetric Cryptol., 2018(4):39–61, 2018.
  * [14] FBI.  Fbi director comments on san bernardino matter, 2016.  https://www.fbi.gov/news/pressrel/press-releases/fbi-director-comments-on-san-bernardino-matter.
  * [15] Google.  Android source: New app lifecycle for encryption, 2016.  https://source.android.com/security/reports/Android-Bootcamp-2016-New-App-Lifecycle-for-Encryption.pdf.
  * [16] Google.  Android source: Authentication, 2018.  https://source.android.com/security/authentication/.
  * [17] Google.  Android source: File-based encryption, 2018.  https://source.android.com/security/encryption/file-based.
  * [18] Google.  Android source: Verified boot, 2018.  https://source.android.com/security/verifiedboot/.
  * [19] Google.  Android source: Metadata encryption, 2019.  https://source.android.com/security/encryption/metadata.
  * [20] Google.  Fscrypt kernel contribution by google, 2020.  https://github.com/google/fscrypt.
  * [21] Michael Halcrow, Uday Savagaonkar, T Ts’o, and I Muslukhov.  Filesystem-level encryption, 2016.  https://www.kernel.org/doc/html/latest/filesystems/fscrypt.html.
  * [22] Michael Austin Halcrow.  ecryptfs: An enterprise-class encrypted filesystem for linux.  In Proceedings of the 2005 Linux Symposium, volume 1, pages 201–218, 2005.
  * [23] Roee Hay and Avi Dayan.  Android keystore stack buffer overflow, 2014.
  * [24] Louiza Khati, Nicky Mouha, and Damien Vergnaud.  Full disk encryption: bridging theory and practice.  In Cryptographers’ Track at the RSA Conference, pages 241–257. Springer, 2017.
  * [25] Logan Koepke, Emma Weil, Urmila Janardan, Tinuola Dada, and Harlan Yu.  Mass extraction: The widespread power of u.s. law enforcement to search mobile phones, 2020.  https://www.upturn.org/reports/2020/mass-extraction/.
  * [26] Ivan Krstić.  Behind the scenes with ios security.  In Blackhat USA, 2016.
  * [27] Junghee Lee, Kalidas Ganesh, Hyuk-Jun Lee, and Youngjae Kim.  Fessd: A fast encrypted ssd employing on-chip access-control memory.  IEEE Computer Architecture Letters, 16(2):115–118, 2017.
  * [28] David A. McGrew and John Viega.  The security and performance of the galois/counter mode (GCM) of operation.  In Anne Canteaut and Kapalee Viswanathan, editors, Progress in Cryptology - INDOCRYPT 2004, 5th International Conference on Cryptology in India, Chennai, India, December 20-22, 2004, Proceedings, volume 3348 of Lecture Notes in Computer Science, pages 343–355. Springer, 2004.
  * [29] Carlo Meijer and Bernard Van Gastel.  Self-encrypting deception: weaknesses in the encryption of solid state drives (ssds).  Radboud University and Open University of the Netherlands, Tech. Rep, 2018.
  * [30] Tilo Müller and Felix C Freiling.  A systematic assessment of the security of full disk encryption.  IEEE Transactions on Dependable and Secure Computing, 12(5):491–503, 2015.
  * [31] Yuichi Niwa, Keisuke Ohashi, Kazuhiko Minematsu, and Tetsu Iwata.  GCM security bounds reconsidered.  In Gregor Leander, editor, Fast Software Encryption - FSE 2015, Revised Selected Papers, volume 9054 of Lecture Notes in Computer Science, pages 385–407. Springer, 2015.
  * [32] Vaibhav Ranchhoddas Pandya.  Iphone securtity analysis.  Journal of Information Security, 2008.
  * [33] Android Open Source Project.  Ext4 encryption, 2020.  https://android.googlesource.com/platform/system/vold/+/a701c458ca6d36604f417f55e95c63493d1545d7.
  * [34] Android Open Source Project.  Keyutil interface, 2020.  https://android.googlesource.com/platform/system/vold/+/master/KeyUtil.cpp.
  * [35] Phillip Rogaway.  Evaluation of some blockcipher modes of operation.  Cryptography Research and Evaluation Committees (CRYPTREC) for the Government of Japan, 2011.
  * [36] Mohamed Sabt and Jacques Traoré.  Breaking into the keystore: A practical forgery attack against android keystore.  In European Symposium on Research in Computer Security, pages 531–548. Springer, 2016.
  * [37] Samsung.  Samsung teegris, 2019.  https://securephones.io/main.pdf.
  * [38] Nigel P. Smart.  Cryptography Made Simple.  Information Security and Cryptography. Springer, 2016.
  * [39] Alexander Tarasikov.  Reverse-engineering samsung exynos 9820 bootloader and tz, 2019.  http://allsoftwaresucks.blogspot.com/2019/05/reverse-engineering-samsung-exynos-9820.html.
  * [40] Peter Teufl, Andreas Fitzek, Daniel Hein, Alexander Marsalek, Alexander Oprisnik, and Thomas Zefferer.  Android encryption systems.  In Privacy and Security in Mobile Systems (PRISMS), 2014 International Conference on, pages 1–8. IEEE, 2014.
  * [41] Peter Teufl, Thomas Zefferer, and Christof Stromberger.  Mobile device encryption systems.  In Security and Privacy Protection in Information Processing Systems, pages 203–216. Springer Berlin Heidelberg, 2013.
  * [42] Peter Teufl, Thomas Zefferer, Christof Stromberger, and Christoph Hechenblaikner.  ios encryption systems: Deploying ios devices in security-critical environments.  In 2013 International Conference on Security and Cryptography (SECRYPT), pages 1–13. IEEE, 2013.
  * [43] Erez Zadok, Ion Badulescu, and Alex Shender.  Cryptfs: A stackable vnode level encryption file system.  Technical report, Technical Report CUCS-021-98, Computer Science Department, Columbia University, 1998.
  * [44] Maximilian Zinkus, Tushar M. Jois, and Matthew Green.  Data security on mobile devices: Current state of the art, open problems, and proposed solutions, 2020.  https://securephones.io/main.pdf.

###  0..1 Proof of security for MFBE

###### Proof

The proof goes by constructing a sequence of games:

Game 0

This game is defined as:

$b\stackrel{{\scriptstyle\$}}{{\leftarrow}}\\{0,1\\};~{}b^{\prime}\leftarrow
Exp^{\mathsf{MFBE},b}_{\mathcal{A}}(1^{\lambda});~{}\mbox{return }b^{\prime}$

Let $S_{0}$ be the event $b^{\prime}=b$ in Game 0. Then we have:

$\displaystyle Adv_{\mathcal{A}}^{\mathsf{MFBE}}$
$\displaystyle=\left\lvert{\mathsf{Pr}\Big{[}\mathrm{Exp}_{\mathcal{A}}^{\mathsf{MFBE},1}=1\Big{]}-\mathsf{Pr}\Big{[}\mathrm{Exp}_{\mathcal{A}}^{\mathsf{MFBE},0}=1\Big{]}}\right\rvert$
$\displaystyle=\left\lvert{\mathsf{Pr}\Big{[}\mathrm{Exp}_{\mathcal{A}}^{\mathsf{MFBE},1}=1\Big{]}+\mathsf{Pr}\Big{[}\mathrm{Exp}_{\mathcal{A}}^{\mathsf{MFBE},0}=0\Big{]}-1}\right\rvert$
$\displaystyle=\left\lvert{2\cdot\mathsf{Pr}\Big{[}S_{0}\Big{]}-1}\right\rvert$

Game 1

This game is the same as Game 0 except the decryption
$DEC^{\sigma\texttt{-}ciph}$ in the oracle $\mathcal{O}^{unwrap}$ is performed
using a table lookup rather than real decryption operation. Formally, we
modify the oracles $\mathcal{O}^{wrap}$ and $\mathcal{O}^{unwrap}$ as below:

$\displaystyle\underline{\mathcal{O}^{wrap}(pol):}$ $\displaystyle
k,w\leftarrow KGen(1^{\lambda})$ $\displaystyle(\phi,\overline{pol})\leftarrow
WrapKey^{\sigma}(k,w,pol)$ $\displaystyle
L_{wrap}=L_{wrap}\cup\\{(k,w,\phi,\overline{pol})\\}$
$\displaystyle\mbox{return }(\phi,\overline{pol})$

The association between $k,w,\phi,\overline{pol}$ is recorded in a list
$L_{wrap}$ which is initialised to be $\emptyset$. Correspondingly, we modify
$\mathsf{UnwrapKey}^{\sigma}(\phi,\overline{pol})$ in the unwrap oracle
$\mathcal{O}^{unwrap}$ as below:

$\displaystyle\underline{\mathsf{UnwrapKey}^{\sigma}(\phi,\overline{pol}):}$
$\displaystyle\mbox{If }(\cdot,w,\cdot,\overline{pol})\in L_{wrap}\mbox{ for
some }w$ $\displaystyle\quad ciph\leftarrow\overline{pol}.cipher$ if pol.usage
= DeviceDataAfterBoot or pol.usage = UserDataAfterBoot then
$\displaystyle\qquad k\leftarrow DEC^{ciph}(\phi,w)$
$\displaystyle\qquad\mbox{return }k$ $\displaystyle\mbox{else return }\bot$

Let $S_{1}$ be the event $b^{\prime}=b$ in Game 1. Let $E$ be the event that
the adversary queries $\mathcal{O}^{unwrap(\cdot,\overline{pol})}$ such that
$DEC^{ciph}(C,\sigma\texttt{-}key)\neq\bot$ and $C$ is not generated by any
$\mathcal{O}^{wrap}$ query, where $C=\overline{pol}.wrapkey$. Since Game 0 and
Game 1 proceed identically unless $E$ occurs, we have
$\left\lvert{\mathsf{Pr}\Big{[}S_{0}\Big{]}-\mathsf{Pr}\Big{[}S_{1}\Big{]}}\right\rvert\leq\mathsf{Pr}\Big{[}E\Big{]}$.

Next we shall prove that $\mathsf{Pr}\Big{[}E\Big{]}\leq
Adv^{CTXT}_{\sigma\mbox{-}ciph,\mathcal{B}_{1}}$. For any adversary
$\mathcal{A}$ that attacks Game 1 and runs in time at most $\tau$, we can
construct an adversary $\mathcal{B}_{1}^{{ENC_{\sigma-
key}^{\sigma\mbox{-}ciph}},{DEC_{\sigma-key}^{\star,\sigma\mbox{-}ciph}}}$
that attacks $\sigma\mbox{-}ciph$ in the INT-CTXT sense and runs in time at
most $\tau$: $\mathcal{B}_{1}$ chooses
$b\stackrel{{\scriptstyle\$}}{{\leftarrow}}\\{0,1\\}$ and runs $\mathcal{A}$
as a subroutine. $\mathcal{B}_{1}$ answers the oracle query
$\mathcal{O}^{wrap}$ queries using its oracle $ENC_{\sigma-
key}^{\sigma\mbox{-}ciph}$ and maintains a list of pairs of queried plaintext
and the returned ciphertext. $\mathcal{B}_{1}$ answers the queries to
$\mathcal{O}^{unwrap}$ using the list to find the corresponding plaintext. For
any ciphertext $C$ that is not in the list, $\mathcal{B}_{1}$ queries to
$DEC_{\sigma-key}^{\star,\sigma\mbox{-}ciph}$. If $DEC_{\sigma-
key}^{\star,\sigma\mbox{-}ciph}(C)=1$, $\mathcal{B}_{1}$ stops; otherwise
$\mathcal{B}_{1}$ returns $\bot$. Therefore we have
$\left\lvert{\mathsf{Pr}\Big{[}S_{0}\Big{]}-\mathsf{Pr}\Big{[}S_{1}\Big{]}}\right\rvert\leq
Adv^{CTXT}_{\sigma\mbox{-}ciph,\mathcal{B}_{1}}$.

Game 2

This game is exactly the same as Game 1 except the wrap key encrypted with
$\sigma\texttt{-}key$ is uniform random $w^{\prime}$. Formally, the oracle
$\mathcal{O}^{wrap}$ is answered as below:

$\displaystyle\underline{\mathcal{O}^{wrap}(pol):}$ $\displaystyle
k,w,w^{\prime}\leftarrow KGen(1^{\lambda})$ $\displaystyle ciph\leftarrow
pol.cipher$ $\displaystyle\overline{pol}\leftarrow pol$ if pol.usage =
DeviceDataAfterBoot or pol.usage = UserDataAfterBoot then
$\displaystyle\quad\phi\leftarrow ENC^{ciph}(k,w)$
$\displaystyle\quad\overline{pol}.wrapkey\leftarrow
ENC^{\sigma\texttt{-}ciph}(w^{\prime},\sigma\texttt{-}key)$
$\displaystyle\quad
L_{wrap}=L_{wrap}\cup\\{(k,w,w^{\prime},\phi,\overline{pol})\\}$
$\displaystyle\quad\mbox{return }(\phi,\overline{pol})$
$\displaystyle\mbox{else return }\bot$

The class key $k$ is encrypted with $w$, while the wrap key encrypted with
$\sigma\texttt{-}key$ is actually $w^{\prime}$. The association between
$k,w,w^{\prime},\phi,\overline{pol}$ is recorded in a list $L_{wrap}$ which is
initialised to be $\emptyset$. Correspondingly, we modify
$\mathsf{UnwrapKey}^{\sigma}(\phi,\overline{pol})$ in the unwrap oracle
$\mathcal{O}^{unwrap}$ as below:

$\displaystyle\underline{\mathsf{UnwrapKey}^{\sigma}(\phi,\overline{pol}):}$
$\displaystyle\mbox{If }(\cdot,w,\cdot,\cdot,\overline{pol})\in L_{wrap}\mbox{
for some }w$ $\displaystyle\quad ciph\leftarrow\overline{pol}.cipher$ if
pol.usage = DeviceDataAfterBoot or pol.usage = UserDataAfterBoot then
$\displaystyle\qquad k\leftarrow DEC^{ciph}(\phi,w)$
$\displaystyle\qquad\mbox{return }k$ $\displaystyle\mbox{else return }\bot$

Let $S_{2}$ be the event $b^{\prime}=b$. We shall prove that
$\left\lvert{\mathsf{Pr}\Big{[}S_{2}\Big{]}-\mathsf{Pr}\Big{[}S_{1}\Big{]}}\right\rvert\leq
Adv_{\sigma\mbox{-}ciph,\mathcal{B}_{2}}^{CPA}$. We construct the IND-CPA
adversary
$\mathcal{B}_{2}^{Enc^{\sigma\mbox{-}ciph}_{\sigma\mbox{-}key}(LR(\cdot,\cdot,d))}$
with $d\in\\{0,1\\}$ that attacks $\sigma\mbox{-}ciph$ as follows.
$\mathcal{B}_{2}$ chooses
$b\stackrel{{\scriptstyle\$}}{{\leftarrow}}\\{0,1\\}$ and runs Game 1.
$\mathcal{B}_{2}$ answers the query to $\mathcal{O}^{wrap}$ by choosing
$k,w,w^{\prime}\stackrel{{\scriptstyle\$}}{{\leftarrow}}KGen(1^{\lambda})$,
$\phi\leftarrow ENC^{ciph}(k,w)$ and queries its left-right oracle to get
$\overline{pol}.wrapkey\leftarrow
Enc^{\sigma\mbox{-}ciph}_{\sigma\texttt{-}key}(LR(w,w^{\prime},d))$.
$\mathcal{B}_{2}$ records $(k,w,w^{\prime},\phi,\overline{pol})$ in the list
$L_{wrap}$. To answer queries to $\mathcal{O}^{unwrap}$ on
$(\phi,\overline{pol})$, $\mathcal{B}_{2}$ checks if
$(\cdot,w,\cdot,\cdot,\overline{pol})\in L_{wrap}$. If so, $\mathcal{B}_{2}$
uses $w$ to decrypt $\phi$. Otherwise $\mathcal{B}_{2}$ returns $\bot$. All
the other oracles can be easily answered since $\mathcal{B}_{2}$ has all the
class keys $k$. $\mathcal{B}_{2}$ outputs $b^{\prime}=b$.

If $d=0$, $\mathcal{B}_{2}$ simulates Game 1 perfectly. If $d=1$,
$\mathcal{B}_{2}$ simulates Game 2 perfectly. Therefore we have

$\displaystyle Adv_{\sigma\mbox{-}ciph,\mathcal{B}_{2}}^{CPA}$
$\displaystyle=\left\lvert{\mathsf{Pr}\Big{[}\mathrm{Exp}_{\sigma\mbox{-}ciph,\mathcal{B}_{2}}^{CPA,1}=1\Big{]}-\mathsf{Pr}\Big{[}\mathrm{Exp}_{\sigma\mbox{-}ciph,\mathcal{B}_{2}}^{CPA,0}=1\Big{]}}\right\rvert$
$\displaystyle=\left\lvert{\mathsf{Pr}\Big{[}S_{2}\Big{]}-\mathsf{Pr}\Big{[}S_{1}\Big{]}}\right\rvert$

Game 3

This game is defined exactly the same as Game 2 except

  * •

Uniformly and randomly select
$\eta\stackrel{{\scriptstyle\$}}{{\leftarrow}}[q_{w}]$ where $q_{w}$ is the
total number of queries to $\mathcal{O}^{wrap}$.

  * •

Let
$(k_{\eta},w_{\eta},w^{\prime}_{\eta},\phi_{\eta},\overline{pol}_{\eta})\in
L_{wrap}$ be the values generated in the $\eta$-th query to
$\mathcal{O}^{wrap}$. In the challenge query, if the key corresponds to
$kid^{\star}$ is not $k_{\eta}$, then aborts.

Let $S_{3}$ be the event $b^{\prime}=b$. Clearly, the probability that abort
does not happen is $1/q_{w}$ since $\eta$ is uniformly and randomly chosen.
When abort does not happen, Game 3 is the same as Game 2. Therefore
$\mathsf{Pr}\Big{[}S_{3}\Big{]}=\mathsf{Pr}\Big{[}S_{2}\Big{]}/q_{w}$.

Game 4

This game is defined exactly the same as Game 3 except:

  * •

Let
$(k_{\eta},w_{\eta},w^{\prime}_{\eta},\phi_{\eta},\overline{pol}_{\eta})\in
L_{wrap}$ be the values generated in the $\eta$-th query to
$\mathcal{O}^{wrap}$. When query $(\phi,\overline{pol}_{\eta})$ to
$\mathcal{O}^{unwrap}$ for some $\phi$, replace the decryption
$DEC^{ciph}(\phi,w_{\eta})$ with the table lookup: if $\phi=\phi_{\eta}$ then
get $k_{\eta}$ from
$(k_{\eta},\cdot,\cdot,\phi_{\eta},\overline{pol}_{\eta})\in L_{wrap}$;
otherwise return $\bot$.

Let $S_{4}$ be the event $b^{\prime}=b$ in Game 4. Let $E$ be the event that
the adversary queries $\mathcal{O}^{unwrap(\phi,\overline{pol}_{\eta})}$ such
that $\phi\neq\phi_{\eta}$ and $DEC^{ciph}(\phi,w_{\eta})\neq\bot$. Since Game
4 and Game 3 are exactly the same unless $E$ happens, we have
$\left\lvert{\mathsf{Pr}\Big{[}S_{4}\Big{]}-\mathsf{Pr}\Big{[}S_{3}\Big{]}}\right\rvert\leq\mathsf{Pr}\Big{[}E\Big{]}$.
We can prove that $\mathsf{Pr}\Big{[}E\Big{]}\leq
Adv_{ciph,\mathcal{B}_{3}}^{CTXT}$ for some adversary $\mathcal{B}_{3}$ that
attacks $ciph$ in the INT-CTXT sense. The proof is similar to the analysis in
Game 1 and is thus omitted. Based on this we can have
$\left\lvert{\mathsf{Pr}\Big{[}S_{4}\Big{]}-\mathsf{Pr}\Big{[}S_{3}\Big{]}}\right\rvert\leq
Adv_{ciph,\mathcal{B}_{3}}^{CTXT}$.

Game 5

This game is defined exactly the same as Game 4 except that the $\eta$-th
query to $\mathcal{O}^{wrap}$ is answered as below:

$\displaystyle\underline{\mathcal{O}^{wrap}(pol_{\eta}):}$ $\displaystyle
k_{\eta},k^{\prime}_{\eta},w_{\eta},w^{\prime}_{\eta}\leftarrow
KGen(1^{\lambda})$ $\displaystyle ciph\leftarrow pol_{\eta}.cipher$
$\displaystyle\overline{pol}_{\eta}\leftarrow pol_{\eta}$ if pol.usage =
DeviceDataAfterBoot or pol.usage = UserDataAfterBoot then
$\displaystyle\quad\phi_{\eta}\leftarrow
ENC^{ciph}(k^{\prime}_{\eta},w_{\eta})$
$\displaystyle\quad\overline{pol}_{\eta}.wrapkey\leftarrow
ENC^{\sigma\mbox{-}ciph}(w^{\prime}_{\eta},\sigma\mbox{-}key)$
$\displaystyle\quad
L_{wrap}=L_{wrap}\cup\\{(k_{\eta},k_{\eta}^{\prime},w_{\eta},w_{\eta}^{\prime},\phi_{\eta},\overline{pol}_{\eta})\\}$
$\displaystyle\quad\mbox{return }(\phi_{\eta},\overline{pol}_{\eta})$
$\displaystyle\mbox{else return }\bot$

And we modify $\mathsf{UnwrapKey}^{\sigma}(\phi_{\eta},\overline{pol}_{\eta})$
in the unwrap oracle $\mathcal{O}^{unwrap}$ on
$(\phi_{\eta},\overline{pol}_{\eta})$ as below:

$\displaystyle\underline{\mathsf{UnwrapKey}^{\sigma}(\phi_{\eta},\overline{pol}_{\eta}):}$
$\displaystyle\mbox{If
}(k_{\eta},\cdot,\cdot,\cdot,\phi_{\eta},\overline{pol}_{\eta})\in L_{wrap}$
$\displaystyle\quad ciph\leftarrow\overline{pol}_{\eta}.cipher$ if pol.usage =
DeviceDataAfterBoot or pol.usage = UserDataAfterBoot then
$\displaystyle\qquad\quad\mbox{return }k_{\eta}$ $\displaystyle\quad\mbox{else
return }\bot$

Note that the above modification is only for the $\eta$-th query, and the
other queries are answered exactly the same as in Game 4. Let $S_{5}$ be the
event $b^{\prime}=b$. Similar to the analysis in Game 2, we can prove that

$\displaystyle Adv_{ciph,\mathcal{B}_{4}}^{CPA}$
$\displaystyle=\left\lvert{\mathsf{Pr}\Big{[}\mathrm{Exp}_{ciph,\mathcal{B}_{4}}^{CPA,1}=1\Big{]}-\mathsf{Pr}\Big{[}\mathrm{Exp}_{ciph,\mathcal{B}_{4}}^{CPA,0}=1\Big{]}}\right\rvert$
$\displaystyle=\left\lvert{\mathsf{Pr}\Big{[}S_{5}\Big{]}-\mathsf{Pr}\Big{[}S_{4}\Big{]}}\right\rvert$

Game 6

This game is exactly the same as Game 5 except the key derivation function
$F_{k_{\eta}}:\\{0,1\\}^{\ell}\mapsto\\{0,1\\}^{n}$ is replaced with a random
function $R$ obtained by
$R\stackrel{{\scriptstyle\$}}{{\leftarrow}}Rand^{\ell\mapsto n}$, where
$k_{\eta}$ is the class key generated in the $\eta$-th query to
$\mathcal{O}^{wrap}$ and $Rand^{\ell\mapsto n}$ is the family of all functions
from $\\{0,1\\}^{\ell}$ to $\\{0,1\\}^{n}$. Let $S_{6}$ be the event
$b^{\prime}=b$. We shall prove

$\left\lvert{\mathsf{Pr}\Big{[}S_{6}\Big{]}-\mathsf{Pr}\Big{[}S_{5}\Big{]}}\right\rvert\leq
Adv^{PRF}_{F,\mathcal{B}_{5}}$

Let $\mathcal{O}_{0}=R$ and $\mathcal{O}_{1}=F_{k_{\eta}}$. We construct the
PRF adversary $\mathcal{B}_{5}^{\mathcal{O}_{d}(\cdot)}$ with $d\in\\{0,1\\}$
as follows. $\mathcal{B}_{5}$ chooses
$b\stackrel{{\scriptstyle\$}}{{\leftarrow}}\\{0,1\\}$ and runs Game 5. When
$\mathcal{B}_{5}$ answers the $\eta$-th query to $\mathcal{O}^{wrap}$,
$\mathcal{B}_{5}$ sets $k_{\eta}=\bot$ which means $\mathcal{B}_{5}$ does not
know the value of $k_{\eta}$. $\mathcal{B}_{5}$ gets the values of
$F_{k_{\eta}}(n_{c})$ in the query $\mathcal{O}^{enc}$ (resp.
$\mathcal{O}^{dec}$) on $(kid,{\textit{f}}node)$ (resp. $(kid,enode)$) with
$kid$ being $k_{\eta}$’s handler by querying $\mathcal{O}_{d}(n_{c})$. When
$k_{\eta}$ corresponds to the class key used in the challenge query which
means abort does not happen, the adversary is not allowed to query
$\mathcal{O}^{reveal}(kid^{\star})$. $\mathcal{B}_{5}$ outputs $b^{\prime}=b$.

If $d=1$, $\mathcal{B}_{5}$ simulates Game 5 perfectly. If $d=0$,
$\mathcal{B}_{5}$ simulates Game 6 perfectly. Therefore we have

$\displaystyle Adv_{F,\mathcal{B}}^{PRF}$
$\displaystyle=\left\lvert{\mathsf{Pr}\Big{[}\mathrm{Exp}_{F,\mathcal{B}_{5}}^{PRF,1}=1\Big{]}-\mathsf{Pr}\Big{[}\mathrm{Exp}_{F,\mathcal{B}_{5}}^{PRF,0}=1\Big{]}}\right\rvert$
$\displaystyle=\left\lvert{\mathsf{Pr}\Big{[}S_{5}\Big{]}-\mathsf{Pr}\Big{[}S_{6}\Big{]}}\right\rvert$

Next we shall prove that

$\displaystyle\left\lvert{2\mathsf{Pr}\Big{[}S_{6}\Big{]}-\frac{1}{q_{w}}}\right\rvert=Adv^{CCA}_{\textit{f}s\mbox{\\_}ciph,\mathcal{B}_{6}}$

for some adversary $\mathcal{B}_{6}$ that attacks $\textit{f}s\mbox{\\_}ciph$
in the IND-CCA sense. Given an adversary $\mathcal{A}$ that attacks Game 6 and
runs in time at most $\tau$, we construct the adversary
$\mathcal{B}_{6}^{\mathcal{E}_{K}(LR(\cdot,\cdot,b)),\mathcal{D}_{K}}$ that
runs in time at most $\tau$ as follows. $\mathcal{B}_{6}$ chooses
$\eta\stackrel{{\scriptstyle\$}}{{\leftarrow}}[q_{w}]$. For the $\eta$-th
query to $\mathcal{O}^{wrap}$, $\mathcal{B}_{6}$ sets $k_{\eta}=\bot$. The key
derivation function $F_{k_{\eta}}$ is replaced with a random table $R$. For
the challenge query $(kid^{\star},{\textit{f}}node_{0},{\textit{f}}node_{1})$,
if $kid^{\star}$ is not the key handler for $k_{\eta}$ then $\mathcal{B}_{6}$
aborts. Otherwise $\mathcal{B}_{6}$ chooses
$n_{c}\stackrel{{\scriptstyle\$}}{{\leftarrow}}\\{0,1\\}^{\ell}$ and
implicitly sets $R[n_{c}]=K$ since $\mathcal{B}_{6}$ does not know $K$.
$\mathcal{B}_{6}$ creates the challenge ciphertext $enode^{\star}$ by setting
$enode^{\star}.meta=n_{c}$ and
$enode^{\star}.content\leftarrow\mathcal{E}_{K}(LR(\allowbreak{\textit{f}}node_{0},{\textit{f}}node_{1},b))$
obtained by querying $\mathcal{B}_{6}$’s left-right encryption oracle. To
answer further encryption query to
$\mathcal{O}^{enc(kid^{\star},{\textit{f}}node)}$ with
${\textit{f}}node.meta=n_{c}$, $\mathcal{B}_{6}$ queries
$e\leftarrow\mathcal{E}_{K}(LR({\textit{f}}node,\allowbreak{\textit{f}}node,b))$
and returns $enode$ with $enode.meta=n_{c}$ and $enode.content=e$. The
decryption query $\mathcal{O}^{dec(kid^{\star},enode)}$ with
$enode.meta=n_{c}$ can be answered by querying $\mathcal{D}_{K}$ when $enode$
is neither $enode^{\star}$ nor obtained from
$\mathcal{O}^{enc(kid^{\star},\cdot)}$. The other queries can be easily
answered and are omitted here because $\mathcal{B}$ selects all other class
keys and file encryption keys. Finally $\mathcal{A}$ outputs $b^{\prime}$ and
$\mathcal{B}_{6}$ outputs $b^{\prime}$.

It is easy to see that $\mathcal{B}_{6}$ simulates Game 6 perfectly. Only when
$\mathcal{B}_{6}$ does not abort, it can output 0/1. Since $\eta$ is uniformly
and randomly chosen, the probability that $\mathcal{B}_{6}$ does not abort is
$1/q_{w}$. Therefore,

$\displaystyle Adv_{\textit{f}s\mbox{\\_}ciph,\mathcal{B}_{6}}^{CCA}$
$\displaystyle=\left\lvert{\mathsf{Pr}\Big{[}\mathrm{Exp}_{\textit{f}s\mbox{\\_}ciph,\mathcal{B}_{6}}^{CCA,1}=1\Big{]}-\mathsf{Pr}\Big{[}\mathrm{Exp}_{\textit{f}s\mbox{\\_}ciph,\mathcal{B}_{6}}^{CCA,0}=1\Big{]}}\right\rvert$
$\displaystyle=\left\lvert{\mathsf{Pr}\Big{[}\mathrm{Exp}_{\textit{f}s\mbox{\\_}ciph,\mathcal{B}_{6}}^{CCA,1}=1\Big{]}-\frac{1}{q_{w}}+\mathsf{Pr}\Big{[}\mathrm{Exp}_{\textit{f}s\mbox{\\_}ciph,\mathcal{B}_{6}}^{CCA,0}=0\Big{]}}\right\rvert$
$\displaystyle=\left\lvert{2\mathsf{Pr}\Big{[}S_{6}\Big{]}-\frac{1}{q_{w}}}\right\rvert$

Combing all the results above, we obtain

$\displaystyle Adv$
${}_{\mathcal{A}}^{\mathsf{MFBE}}=\left\lvert{2\cdot\mathsf{Pr}\Big{[}S_{0}\Big{]}-1}\right\rvert$
$\displaystyle\leq
2Adv_{\sigma\mbox{-}ciph,\mathcal{B}_{1}}^{CTXT}+2Adv_{\sigma\mbox{-}ciph,\mathcal{B}_{2}}^{CPA}+2q_{w}Adv_{ciph,\mathcal{B}_{3}}^{CTXT}$
$\displaystyle\quad+2q_{w}Adv_{ciph,\mathcal{B}_{4}}^{CPA}+2q_{w}Adv_{F,\mathcal{B}_{5}}^{PRF}+q_{w}Adv_{\textit{f}s\mbox{\\_}ciph,\mathcal{B}_{6}}^{CCA}$

This completes the proof.

###  0..2 Security definitions for symmetric ciphers

######  Definition 4 (IND-CPA and IND-CCA [6])

Let $\mathcal{S}\mathcal{E}=(\mathcal{K},\mathcal{E},\mathcal{D})$ be a
symmetric encryption scheme. Let $b\in\\{0,1\\}$ and $\mathcal{A}$ be an
adversary. We define the left-right oracle
$\mathcal{O}^{\mathcal{E}_{k}(\mathcal{L}\mathcal{R}(\cdot,\cdot,b))}$, to
take input $(x_{0},x_{1})$ and return $\mathcal{E}_{k}(x_{b})$, and we write
$\mathcal{O}^{\mathcal{D}_{k}(\cdot)}$ for the decryption oracle. Consider the
following experiments:

$\begin{array}[]{l}\mathrm{Exp}_{\mathcal{S}\mathcal{E},\mathcal{A}}^{CPA,b}(1^{\lambda}):\\\ \quad k\stackrel{{\scriptstyle\$}}{{\leftarrow}}\mathcal{K}(1^{\lambda})\\\ \quad b^{\prime}\leftarrow\mathcal{A}^{\mathcal{O}^{\mathcal{E}_{k}(\mathcal{L}\mathcal{R}(\cdot,\cdot,b))}}(1^{\lambda})\\\ \quad\mbox{return }b^{\prime}\end{array}$ |  $\begin{array}[]{l}\mathrm{Exp}_{\mathcal{S}\mathcal{E},\mathcal{A}}^{CCA,b}(1^{\lambda}):\\\ \quad k\stackrel{{\scriptstyle\$}}{{\leftarrow}}\mathcal{K}(1^{\lambda})\\\ \quad b^{\prime}\leftarrow\mathcal{A}^{\mathcal{O}^{\mathcal{E}_{k}(\mathcal{L}\mathcal{R}(\cdot,\cdot,b))},\mathcal{O}^{\mathcal{D}_{k}(\cdot)}}(1^{\lambda})\\\ \quad\mbox{return }b^{\prime}\end{array}$
---|---

In the CCA experiment, the adversary cannot query
$\mathcal{O}^{\mathcal{D}_{k}(\cdot)}$ on a ciphertext output by
$\mathcal{O}^{\mathcal{E}_{k}(\mathcal{L}\mathcal{R}(\cdot,\cdot,b))}$. We
define the advantages of the adversaries via

$\displaystyle Adv_{\mathcal{S}\mathcal{E},\mathcal{A}}^{CPA}(1^{\lambda})$
$\displaystyle=\left\lvert{\mathsf{Pr}\Big{[}\mathrm{Exp}_{\mathcal{S}\mathcal{E},\mathcal{A}}^{CPA,1}(1^{\lambda})=1\Big{]}-\mathsf{Pr}\Big{[}\mathrm{Exp}_{\mathcal{S}\mathcal{E},\mathcal{A}}^{CPA,0}(1^{\lambda})=1\Big{]}}\right\rvert$
$\displaystyle Adv_{\mathcal{S}\mathcal{E},\mathcal{A}}^{CCA}(1^{\lambda})$
$\displaystyle=\left\lvert{\mathsf{Pr}\Big{[}\mathrm{Exp}_{\mathcal{S}\mathcal{E},\mathcal{A}}^{CCA,1}(1^{\lambda})=1\Big{]}-\mathsf{Pr}\Big{[}\mathrm{Exp}_{\mathcal{S}\mathcal{E},\mathcal{A}}^{CCA,0}(1^{\lambda})=1\Big{]}}\right\rvert$

The scheme $\mathcal{S}\mathcal{E}$ is said to be IND-CPA (resp. IND-CCA)
secure if the advantage
$Adv_{\mathcal{S}\mathcal{E},\mathcal{A}}^{CPA}(1^{\lambda})$ (resp.
$Adv_{\mathcal{S}\mathcal{E},\mathcal{A}}^{CCA}(1^{\lambda})$) is negligible
for any PPT adversary $\mathcal{A}$.

######  Definition 5 (Finite pseudorandom functions (PRFs))

Given a family of functions
$F:Keys(F)\times\\{0,1\\}^{\ell}\mapsto\\{0,1\\}^{n}$, we write
$f\stackrel{{\scriptstyle\$}}{{\leftarrow}}F$ for the operations
$K\stackrel{{\scriptstyle\$}}{{\leftarrow}}Keys(F),f\leftarrow F_{K}$, which
means selecting a random function $f$ from the family $F$. We write
$Rand^{\ell\mapsto n}$ the family of all functions from $\\{0,1\\}^{\ell}$ to
$\\{0,1\\}^{n}$. Let $b\in\\{0,1\\}$. Consider the following experiment:

$\displaystyle\mathrm{Exp}$ ${}_{F,\mathcal{A}}^{PRF,b}:$
$\displaystyle\mathcal{O}_{0}\stackrel{{\scriptstyle\$}}{{\leftarrow}}Rand^{\ell\mapsto
n};\mathcal{O}_{1}\stackrel{{\scriptstyle\$}}{{\leftarrow}}F$ $\displaystyle
b^{\prime}\leftarrow\mathcal{A}^{\mathcal{O}_{b}(\cdot)}$
$\displaystyle\mbox{return }b^{\prime}$

We define the advantage of the adversary via

$\displaystyle\footnotesize Adv_{F,\mathcal{A}}^{PRF}$
$\displaystyle=\left\lvert{\mathsf{Pr}\Big{[}\mathrm{Exp}_{F,\mathcal{A}}^{PRF,1}=1\Big{]}-\mathsf{Pr}\Big{[}\mathrm{Exp}_{F,\mathcal{A}}^{PRF,0}=1\Big{]}}\right\rvert$

######  Definition 6 (Integrity of ciphertext (INT-CTXT) [7])

Let $\mathcal{S}\mathcal{E}=(\mathcal{K},\mathcal{E},\mathcal{D})$ be a
symmetric encryption scheme. Let $b\in\\{0,1\\}$ and $\mathcal{A}$ be an
adversary. Consider the following experiments:

$\displaystyle\footnotesize\mathrm{Exp}$
${}_{\mathcal{S}\mathcal{E},\mathcal{A}}^{CTXT}(1^{\lambda}):$ $\displaystyle
k\stackrel{{\scriptstyle\$}}{{\leftarrow}}\mathcal{K}(1^{\lambda});S\leftarrow\emptyset$
$\displaystyle\mbox{If
}\mathcal{A}^{\mathcal{O}^{\mathcal{E}_{k}(\cdot)},\mathcal{O}^{\mathcal{D}^{\star}_{k}(\cdot)}}\mbox{
queries to }\mathcal{O}^{\mathcal{D}^{\star}_{k}(C)}s.t.$
$\displaystyle\quad\mathcal{D}_{k}(C)=M\neq\bot$ $\displaystyle\quad\mbox{and
}\mathcal{O}^{\mathcal{E}_{k}(\cdot)}\mbox{ never return }C$ then return 1,
else return 0

We define the advantage of the adversary via

$\displaystyle\footnotesize
Adv_{\mathcal{S}\mathcal{E},\mathcal{A}}^{CTXT}(1^{\lambda})$
$\displaystyle=\mathsf{Pr}\Big{[}\mathrm{Exp}_{\mathcal{S}\mathcal{E},\mathcal{A}}^{CTXT}(1^{\lambda})=1\Big{]}$

The scheme $\mathcal{S}\mathcal{E}$ is said to be INT-CTXT secure if the
advantage $Adv_{\mathcal{S}\mathcal{E},\mathcal{A}}^{CTXT}(1^{\lambda})$ is
negligible for any PPT adversary $\mathcal{A}$.

###  0..3 Algorithms

Input: $enode,kid$

Output: $\textit{f}node$

1

2function  _$\mathsf{\mathsf{Decrypt}}(enode,kid)$_

3 $k_{m}\xleftarrow{}{}GetKeyFromKernelKeyring(kid)$

4 if  _$k$_ then

5 $n\xleftarrow{}\textit{e}node.meta$

6

7 if  _$enode.type=directory$_ then

8 $k_{d}\xleftarrow{}KDF(k_{m},n,mode)$

9
$\textit{f}node.children\xleftarrow{}DEC^{\textit{f}}s\mbox{\\_}ciph(enode.children,k_{d})$

10

11

12 if  _$enode.type=file$_ then

13 $k_{d}\xleftarrow{}KDF(k_{m},n,mode)$

14
$\textit{f}node.content\xleftarrow{}DEC^{\textit{f}}s\mbox{\\_}ciph(enode.content,k_{d})$

15

16 return $\textit{f}node$

17 else

18 return $\bot$

19

Algorithm 9 File decryption in EXT4 filesystems (Android & *NIX systems)

1

Input: $k$

Output: $kid$

2 function  _$\mathsf{ProvisionKey}(k)$_

3 $kid\xleftarrow{}Load(k)$

4 return $kid$

Algorithm 10 $\mathsf{ProvisionKey}$ (Android & iOS)

1

Input: $kid$

Output: $\\{1,\bot\\}$

2 function  _$\mathsf{EvictKey}(kid)$_

3 $ret\xleftarrow{}Clear(kid)$

4 return $ret$

Algorithm 11 $\mathsf{EvictKey}$

1

Input: $econtent,k$

Output: $content$

2 function  _$DEC^{\textit{f}s\mbox{\\_}ciph}(econtent,k)$_

3 for  _$eblock\in econtent$_ do

4 $\mathsf{iv}\xleftarrow{}\mathsf{GetIV}(eblock,k.mode)$

5 $cblock\xleftarrow{}CIPHER(eblock,k.\mathsf{val},\mathsf{iv})$

6 $content\xleftarrow{}content\|cblock$

7

8

9

Algorithm 12 Node content decrypt (Android & *NIX systems)