11institutetext: Stevens Institute of Technology 22institutetext: Inria
Type-based Declassification for Free (with appendix)
Minh Ngo
1122
David A. Naumann
11
Tamara Rezk
22
Abstract
This work provides a study to demonstrate the potential of
using off-the-shelf programming languages
and their theories
to build sound language-based-security tools.
Our study focuses on information flow security
encompassing declassification policies that allow us to express
flexible security policies needed for practical requirements.
We translate security policies, with declassification,
into an interface for which an unmodified standard typechecker
can be applied to a source program—if the program typechecks, it provably satisfies the policy.
Our proof reduces security soundness—with declassification—to the mathematical foundation of data abstraction, Reynolds’ abstraction theorem.
To appear in ICFEM 2020
1 Introduction
A longstanding challenge for software systems is the enforcement of security in applications implemented in conventional general-purpose programming languages.
For high assurance, precise mathematical definitions are needed for policies, enforcement mechanism, and program semantics. The latter, in particular, is a major challenge for languages in practical use. In order to minimize the cost of assurance, especially over time as systems evolve, it is desirable to leverage work on formal modeling with other goals such as functional verification, equivalence checking, and compilation.
To be auditable by stakeholders, policy should be expressed in an accessible way.
This is one of several reasons why types play an important role in many works on information flow (IF) security.
For example, Flowcaml [36] and Jif [29] express policy using types that include IF labels.
They statically enforce policy using dedicated IF type checking and inference.
Techniques from type theory are also used in security proofs such as those for Flowcaml and the calculus DCC [1].
IF is typically formalized as the preservation of indistinguishability relations between executions.
Researchers have hypothesized that this should be
an instance of a celebrated semantics basis in type theory: relational parametricity [39].
Relational parametricity
provides an effective basis for formal reasoning about program transformations
(“theorems for free” [53]),
representation independence and information hiding for program verification [28, 6].
The connection between IF and relational parametricity has been made precise in 2015, for DCC, by translation to the calculus Fω and use of the existing parametricity
theorem for Fω [12].
The connection is also made, perhaps more transparently, in a translation of DCC to dependent type theory,
specifically the calculus of constructions and its parametricity theorem [4].
In this work, we advance the state of the art in the connection between IF and relational parametricity,
guided by three main goals.
One of the goals motivating our work is to reduce the burden of defining dedicated type checking, inference, and security proofs for high assurance in programming languages.
A promising approach towards this goal is the idea of leveraging type abstraction to enforce policy, and in particular, leveraging the parametricity theorem
to obtain security guarantees.
A concomitant goal is to do so for practical IF policies
that encompass selective declassification, which is needed for most policies in practice.
For example, a password checker program or a program that calculates aggregate or statistical information must be considered insecure
without declassification.
To build on the type system and theory of a language without a priori IF features, policy needs to be encoded somehow, and the program may need to be transformed.
For example, to prove that a typechecked DCC term is secure with respect to the policy expressed by its type,
Bowman and Ahmed [12] encode the typechecking judgment by nontrivial
translation of both types and terms into Fω.
Any translation becomes part of the assurance argument.
Most likely, complicated translation will also make it more difficult to use extant
type checking/inference (and other development tools) in diagnosing security errors and developing secure code.
This leads us to highlight a third goal, needed to achieve the first goal, namely to
minimize the complexity of translation.
There is a major impediment to leveraging type abstraction: few languages are relationally parametric or have parametricity theorems.
The lack of parametricity can be addressed by focusing on well behaved subsets and leveraging additional features like ownership types that may be available for other purposes
(e.g., in the Rust language).
As for the paucity of parametricity theorems, we take hope in the recent advances in machine-checked metatheory, such as correctness of the CakeML and CompCert compilers,
the VST logic for C, the relational logic of Iris.
For parametricity specifically, the most relevant work is Crary’s formal proof of parametricity for the ML module calculus [14].
Contributions.
Our first contribution is to translate policies with declassification—in the style of relaxed noninterference [27]—into abstract types in a functional language, in such a way that
typechecking the original program implies its security. For doing so, we neither rely on a specialized security type system [12] nor on modifications of existing type systems [17].
A program that typechecks may use the secret inputs parametrically, e.g., storing in data structures, but cannot look at the data until declassification has been applied.
Our second contribution is to prove security by direct application of a parametricity theorem.
We carry out this development for the polymorphic lambda calculus, using the original theorem of Reynolds.
We also provide an appendix that shows this development for the ML module calculus using Crary’s theorem [14], enabling the use of ML to check security.
2 Background: Language and Abstraction Theorem
To present our results we choose the simply typed and call-by-value lambda calculus, with integers and type variables, for two reasons: (1) the chosen language is similar to the language used in the paper of Reynolds [39] where the abstraction theorem was first proven, and (2) we want to illustrate our encoding approach (§4) in a minimal calculus. This section defines the language we use and recalls the abstraction theorem, a.k.a. parametricity.
Our language is very close to the one in Reynolds [39, § 2]; we prove the abstraction theorem using contemporary notation.111
Some readers may find it helpful to consult the following references for background on logical relations and parametricity: [25, Chapt. 49],
[28, Chapt. 8],
[13],
[34].
Language.
The syntax of the language is as below, where α denotes a type variable, x a term variable, and n an integer value.
A value is closed when there is no free term variable in it.
A type is closed when there is no type variable in it.
[TABLE]
We use small-step semantics, with the reduction relation \rightarrowtriangle defined inductively by these rules.
{mathpar}
\inferrule
πi⟨v1,v2⟩\rightarrowtrianglevi\inferrule
(λx:τ.e)v\rightarrowtrianglee[x↦v] \inferrulee\rightarrowtrianglee′
E[e]\rightarrowtriangleE[e′]
We write e[x↦e′] for capture-avoiding substitution of e′ for free occurrences of x in e.
We use parentheses to disambiguate term structure and write
\rightarrowtriangle∗ for the reflexive, transitive closure of
\rightarrowtriangle.
A typing context Δ is a set of type variables.
A term context Γ is a mapping from term variables to types,
written like x:int,y:int→int.
We write Δ⊢τ to mean that τ is well-formed w.r.t. Δ,
that is, all type variables in τ are in Δ.
We say that e is typable w.r.t. Δ and Γ (denoted by Δ,Γ⊢e) when there exists a well-formed type τ such that Δ,Γ⊢e:τ.
The derivable typing judgments are defined inductively in Fig. 1.
The rules are to be instantiated only with Γ that is well-formed under Δ,
in the sense that Δ⊢Γ(x) for all x∈dom(Γ).
When the term context and the type context are empty, we write ⊢e:τ.
Logical relation.
The logical relation is a type-indexed family of relations on values,
parameterized by given relations for type variables.
From it, we derive a relation on terms.
The abstraction theorem says the latter is reflexive.
Let γ be a term substitution, i.e., a finite map from term variables to closed values, and δ be a type substitution, i.e., a finite map from type variables to closed types. In symbols:
[TABLE]
We say γ respects Γ (denoted by γ⊨Γ)
when dom(γ)=dom(Γ) and ⊢γ(x):Γ(x) for any x.
We say δ respects Δ (denoted by δ⊨Δ)
when dom(δ)=Δ.
Let Rel(τ1,τ2) be the set of all binary relations over closed values of closed types τ1 and τ2.
Let ρ be an environment, a mapping from type variables to relations
R∈Rel(τ1,τ2).
We write ρ∈Rel(δ1,δ2)
to say that ρ is compatible with δ1,δ2 as follows:
ρ∈Rel(δ1,δ2)≜dom(ρ)=dom(δ1)=dom(δ2)∧∀α∈dom(ρ).ρ(α)∈Rel(δ1(α),δ2(α)).
The logical relation is inductively defined in Fig. 2, where ρ∈Rel(δ1,δ2) for some δ1 and δ2.
For any τ, [[τ]]ρ is a relation on closed values.
In addition, [[τ]]ρev is a relation on terms.
Lemma 1
Suppose that ρ∈Rel(δ1,δ2) for some δ1 and δ2.
For i∈{1,2}, it follows that:
if ⟨v1,v2⟩∈[[τ]]ρ, then ⊢vi:δi(τ), and**
if ⟨e1,e2⟩∈[[τ]]ρev, then ⊢ei:δi(τ)**.
We write δ(Γ) to mean a term substitution obtained from Γ by applying δ on the range of Γ, i.e.:
[TABLE]
Suppose that Δ,Γ⊢e:τ, δ⊨Δ, and γ⊨δ(Γ).
Then we write δγ(e) to mean the application of γ and then δ to e.
For example, suppose that δ(α)=int, γ(x)=n for some n, and α,x:α⊢λy:α.x:α→α, then δγ(λy:α.x)=λy:int.n.
We write ⟨γ1,γ2⟩∈[[Γ]]ρ for some ρ∈Rel(δ1,δ2) when γ1⊨δ1(Γ), γ2⊨δ2(Γ), and ⟨γ1(x),γ2(x)⟩∈[[Γ(x)]]ρ
for all x∈dom(Γ).
Definition 1 (Logical equivalence)
Terms e and e′ are logically equivalent at τ in Δ and Γ (written Δ,Γ⊢e∼e′:τ) if Δ,Γ⊢e:τ, Δ,Γ⊢e′:τ, and for all δ1,δ2⊨Δ, all ρ∈Rel(δ1,δ2), and all ⟨γ1,γ2⟩∈[[Γ]]ρ,
we have
⟨δ1γ1(e),δ2γ2(e′)⟩∈[[τ]]ρev.
Theorem 2.1 (Abstraction [39])
If Δ,Γ⊢e:τ, then Δ,Γ⊢e∼e:τ.
3 Declassification Policies
Confidentiality policies can be expressed by
information flows of confidential sources to public sinks in programs.
Confidential sources correspond to the secrets that the program receives and public sinks correspond
to any results given to a public observer, a.k.a. the attacker.
These flows can either be direct —e.g. if
a function, whose result is public, receives a confidential value as input and directly returns the secret—
or indirect —e.g. if a function, whose result is public, receives a confidential boolean value and returns
0 if the confidential value is false and 1 otherwise.
Classification of program sources as confidential or public, a.k.a. security policy, must be given by the programmer or security engineer: for a given security policy the program is said to be secure for noninterference if public resources do not depend on confidential ones. Thus, noninterference for a program means total independence between
public and confidential information.
As simple and elegant as this information flow policy is, noninterference does not permit to consider
as secure programs that purposely need to release information in a controlled way: for example a password-checker function that receives as confidential input a boolean value representing if the system password is equal to the user’s input and returns 0 or 1 accordingly.
In order to consider such intended dependences of public sinks from confidential sources, we need to consider
more relaxed security policies than noninterference, a.k.a. declassification policies.
Declassification security policies allow us to specify controlled ways to release confidential inputs [42].
Declassification policies that we consider in this work map confidential inputs to functions, namely declassification functions. These functions allow the programmer to specify what and how information can be released.
The formal syntax for declassification functions in this work is given
below,222In this paper, the type of confidential inputs is int.
where n is an integer value, and ⊕ represents primitive arithmetic operators.
[TABLE]
The static and dynamic semantics are standard.
To simplify the presentation we suppose that the applications of primitive operators on well-typed arguments terminates.
Therefore, the evaluations of declassification functions on values terminate. A policy simply defines which are the confidential variables and their authorized declassifications.
For policies we refrain from using concrete syntax and instead give a simple
formalization that facilitates later definitions.
Definition 2 (Policy)
A policy P is a tuple ⟨VP,FP⟩, where VP is a finite set of variables for confidential inputs, and FP is a partial mapping from variables in VP to declassification functions.
For simplicity we require that if f appears in the policy then
it is a closed term of type int→τf for some τf.
In the definition of policies, if a confidential input is not associated with a declassification function, then it cannot be declassified.
Example 1 (Policy POE using f)
Consider policy POE given by ⟨VPOE,FPOE⟩ where VPOE={x}
and FPOE(x)=f=λx:int.xmod2.
Policy POE states that only the parity of the confidential input x can be released to a public observer.
4 Type-based Declassification
In this section, we show how to encode declassification policies as standard types in the language of § 2, we define and we prove our free theorem.
We consider a termination-sensitive [32] information flow security property,333Our security property is termination sensitive but programs in the language always terminate.
In the development for ML (in an appendix), programs may not terminate and the security property is also termination sensitive.
with declassification, called type-based relaxed noninterference (TRNI) and taken from Cruz et al [17].
It is important to notice that our developement, in this section,
studies the reuse for security of standard programming languages type systems
together with soundness proofs for security for free by using the abstraction theorem.
In contrast, Cruz et al [17]
use a modified type system for security and prove soundness from scratch, without apealing to parametricity.
Through this section, we consider a fixed policy P (see Def. 2) given by ⟨VP,FP⟩.
We treat free variables in a program as inputs and, without loss of generality, we assume that there are two kinds of inputs: integer values, which are considered as confidential, and declassification functions, which are fixed according to policy. A public input can be encoded as a confidential input that can be declassified via the identity function.
We consider terms without type variables as source programs.
That is we consider terms e s.t. for all type substitutions δ, δ(e) is syntactically the same as e.444An example of a term with type variables is λx:α.x. We can easily check that there exists a type substitutions δ s.t. δ(e) is syntactically different from e (e.g. for δ s.t. δ(α)=int, δ(e)=λx:int.x).
4.1 Views and indistinguishability
We provide two term contexts to define TRNI, called the confidential view and public view. The first view represents an observer that can access confidential inputs, while the second one represents an observer that can only observe declassified inputs.
The views are defined using fresh term and type variables.
Confidential view.
Let V⊤={x ∣ x∈VP∖dom(FP)} be the set of inputs that cannot be declassified.
First we define the encoding for these inputs as a term context:
[TABLE]
Next, we specify the encoding of confidential inputs that can be declassified.
To this end, define ⟨⟨_,_⟩⟩C as follows,
where f:int→τf is in P.
[TABLE]
Finally, we write ΓCP for the term context encoding the confidential view for P.
[TABLE]
We assume that, for any x, the variable xf in the result of ⟨⟨x,FP(x)⟩⟩C is
distinct from the variables in VP, distinct from each other,
and distinct from xf′ for distinct f′.
We make analogous assumptions in later definitions.
From the construction, ΓCP is a mapping, and for any x∈dom(ΓCP), it follows that ΓCP(x) is a closed type.
Therefore, ΓCP is well-formed for the empty set of type variables, so it can be used in typing judgments of the form ΓCP⊢e:τ.
Example 2 (Confidential view)
For POE in Example 1, the confidential view is: ΓCPOE=x:int,xf:int→int.
Public view.
The basic idea is to encode policies by using type variables.
First we define the encoding for confidential inputs that cannot be declassified.
We define a set of type variables, ΔP,⊤P
and a mapping ΓP,⊤P
for confidential inputs that cannot be declassified.
[TABLE]
This gives the program access to x at an opaque type.
In order to define the encoding for confidential inputs that can be declassified,
we define ⟨⟨_,_⟩⟩P:
[TABLE]
The first form will serve to give the program access to x only via function variable xf that we will
ensure is interpreted as the policy function f.
We define a type context ΔPP and term context ΓPP
that comprise the public view, as follows.
[TABLE]
where ⟨S1,S1′⟩∪⟨S2,S2′⟩=⟨S1∪S2,S1′∪S2′⟩.
Example 3 (Public view)
For POE, the typing context in the public view has one type variable: ΔPPOE=αf.
The term context in the public view is ΓPPOE=x:αf, xf:αf→int.
From the construction, ΓPP is a mapping, and for any x∈dom(ΓPP), it follows that ΓPP(x) is well-formed in ΔPP (i.e. ΔPP⊢ΓPP(x)).
Thus, ΓPP is well-formed in the typing context ΔPP.
Therefore, ΔPP and ΓPP can be used in typing judgments of the form ΔPP,ΓPP⊢e:τ.
Notice that in the public view of a policy, types of variables for confidential inputs are not int. Thus, the public view does not allow programs where concrete declassifiers are applied to confidential input variables even when the applications are semantically correct according to the policy (e.g. for POE, the program f x does not typecheck in the public view).
Instead, programs should apply named declassifers (e.g. for POE, the program xf x is well-typed in the public view).
Indistinguishability.
The security property TRNI is defined in a usual way,
using partial equivalence relations called indistinguishability.
To define indistinguishability, we define a type substitution δP such that
δP⊨ΔPP, as follows:
[TABLE]
The inductive definition of indistinguishability for a policy P is presented in Figure 3, where αx and αf are from ΔPP.
Indistinguishability is defined for τ s.t. ΔPP,ΓPP⊢τ.
The definitions of indistinguishability for int and τ1×τ2 are straightforward.
We say that two functions are indistinguishable at τ1→τ2 if on any indistinguishable inputs they generate indistinguishable outputs.
Since we use αx to encode confidential integer values that cannot be declassified, any integer values v1 and v2 are indistinguishable, according to rule Eq-Var1.
Notice that δP(αx)=int.
Since we use αf to encode confidential integer values that can be declassified via f where ⊢f:int→τf, we say that ⟨v1,v2⟩∈IV[[αf]] when ⟨f v1,f v2⟩∈IE[[τf]].
Example 4 (Indistinguishability)
For POE (of Example 1),
two values v1 and v2 are indistinguishable at αf when both of them are even numbers or odd numbers.
[TABLE]
We write e1=inte2 to mean that e1\rightarrowtriangle∗v and e2\rightarrowtriangle∗v for some integer value v.
Term substitutions γ1 and γ2 are called indistinguishable w.r.t. P (denoted by ⟨γ1,γ2⟩∈IV[[P]]) if the following hold.
γ1⊨δP(ΓPP) and γ2⊨δP(ΓPP),
for all xf∈dom(ΓPP), γ1(xf)=γ2(xf)=f,
for all other x∈dom(ΓPP), ⟨γ1(x),γ2(x)⟩∈IV[[ΓPP(x)]].
Note that each γi maps xf to the specific function f in the policy.
Input variables are mapped to indistinguishable values.
We now define type-based relaxed noninterference w.r.t. P for a type τ well-formed in ΔPP.
It says that indistinguishable inputs lead to indistinguishable results.
Definition 3
A term e is TRNI(P,τ) provided that ΓCP⊢e, and ΔPP⊢τ, and for all
⟨γ1,γ2⟩∈IV[[P]]
we have ⟨γ1(e),γ2(e)⟩∈IE[[τ]].
Notice that if a term is well-typed in the public view then by replacing all type variables in it with int, we get a term which is also well-typed in the confidential view (that is, if ΔPP,ΓPP⊢e:τ, then ΓCP⊢δ(e):δ(τ) where δ maps all type variables in ΔPP to int).
However,
Definition 3 also requires that the term e is itself well-typed in the confidential view.
This merely ensures that the definition is applied, as intended, to programs that do not contain type variables.
The definition of TRNI is indexed by a type for the result of the term.
The type can be interpreted as constraining the observations to be made by the public observer.
We are mainly interested in concrete output types, which express that the observer can do whatever they like and has full knowledge of the result.
Put differently, TRNI for an abstract type expresses security under the assumption that the observer is somehow forced to respect the abstraction.
Consider the policy POE (of Example 1) where x can be declassified via f=λx:int.xmod2.
As described in Example 3, ΔPPOE=αf and ΓPPOE=x:αf, xf:αf→int.
We have that the program x is TRNI(POE,αf) since the observer cannot do anything to x except for applying f to x which is allowed by the policy.
This program, however, is not TRNI(POE,int) since the observer can apply any function of the type int→τ′ (for some closed τ′), including the identity function, to x and hence can get the value of x.
Example 5
The program xf x is TRNI(POE,int).
Indeed, for any arbitrary ⟨γ1,γ2⟩∈IV[[P]], we have that γ1(xf)=γ2(xf)=f=λx:int.xmod2, and ⟨v1,v2⟩∈IV[[αf]], where γ1(x)=v1 and γ2(x)=v2 for some v1 and v2.
When we apply γ1 and γ2 to the program, we get respectively v1mod2 and v2mod2.
Since ⟨v1,v2⟩∈IV[[αf]], as described in Example 4, (v1mod2)=int(v2mod2).
Thus, ⟨γ1(xf x),γ2(xf x)⟩∈IE[[int]].
Therefore, the program xf x satisfies the definition of TRNI.
4.2 Free theorem: typing in the public view implies security
In order to prove security “for free”, i.e., as consequence of Theorem 2.1,
we define ρP as follows:
for all αx∈ΔPP, ρP(αx)=IV[[αx]],
for all αf∈ΔPP, ρP(αf)=IV[[αf]].
It is a relation on the type substitution δP defined in Eqn. (1).
Lemma 2
ρP∈Rel(δP,δP).
From Lemma 2, we can write [[τ]]ρP or [[τ]]ρPev for any τ such that ΔPP⊢τ.
We next establish the relation between [[τ]]ρev and IE[[τ]]:
under the interpretation corresponding to the desired policy P, they are equivalent.
In other words, indistinguishability is an instantiation of the logical relation.
Lemma 3
For any τ such that ΔPP⊢τ, we have
⟨v1,v2⟩∈[[τ]]ρP\mboxiff⟨v1,v2⟩∈IV[[τ]],
and also
⟨e1,e2⟩∈[[τ]]ρPev\mboxiff⟨e1,e2⟩∈IE[[τ]].
By analyzing the type of ΓPP(x), we can establish the relation of γ1 and γ2 when ⟨γ1,γ2⟩∈IV[[P]].
Lemma 4
If ⟨γ1,γ2⟩∈IV[[P]], then ⟨γ1,γ2⟩∈[[ΓPP]]ρP.
The main result of this section is that a term is TRNI at τ if it has type τ in the public view that encodes the policy.
Theorem 4.1
If e has no type variables and ΔPP,ΓPP⊢e:τ, then e is TRNI(P,τ).
Proof
From the abstraction theorem (Theorem 2.1), for all δ1,δ2⊨ΔPP, for all ⟨γ1,γ2⟩∈[[ΓPP]]ρ, and for all ρ∈Rel(δ1,δ2), it follows that
[TABLE]
Consider ⟨γ1,γ2⟩∈IV[[P]].
Since ⟨γ1,γ2⟩∈IV[[P]], from Lemma 4, we have that ⟨γ1,γ2⟩∈[[ΓPP]]ρP.
Thus, we have that ⟨δPγ1(e),δPγ2(e)⟩∈[[τ]]ρPev.
Since e has no type variable, we have that δPγi(e)=γi(e).
Therefore, ⟨γ1(e),γ2(e)⟩∈[[τ]]ρPev.
Since ⟨γ1(e),γ2(e)⟩∈[[τ]]ρPev, from Lemma 3, it follows that ⟨γ1(e),γ2(e)⟩∈IE[[τ]].
In addition, since e has no type variable and ΔPP,ΓPP⊢e:τ, we have that δP(ΓPP)⊢e:δP(τ) and hence, ΓCP⊢e.
Therefore, e is TRNI(P,τ).
Example 6 (Typing implies TRNI)
Consider the policy POE. As described in Examples 2 and 3, the confidential view
ΓCPOE is x:int,xf:int→int
and the public view ΔPPOE,ΓPPOE is
αf,x:αf,xf:αf→int.
We look at the program xf x.
We can easily verify that ΓCPOE⊢xf x:int and ΔPPOE,ΓPPOE⊢xf x:int.
Therefore, by Theorem 4.1, the program is TRNI(POE,int).
Example 7
If a program is well-typed in the confidential view but not TRNI(P,τ) for some τ well-formed in the public view of P, then the type of the program in the public view is not τ or the program is not well-typed in the public view.
In policy POE, from Example 6, the public view is αf,x:αf,xf:αf→int.
We first look at the program x that is not TRNI(POE,int) since x itself is confidential and cannot be directly declassified.
In the public view of the policy,
the type of this program is αf which is not int.
We now look at the program xmod3 that
is not TRNI(POE,αf) since it takes indistinguishable inputs at αf (e.g. 2 and 4) and produces results that are not indistinguishable at αf (e.g. 2=2mod3, 1=4mod3, and ⟨2,1⟩∈IV[[αf]]).
We can easily verify that this program is not well-typed in the public view since the type of x in the public view is αf, while mod expects arguments of the int type.
Remark 1 (Extension)
Our encoding can be extended to support richer policies (details in appendix).
To support policies where an input x can be declassified via two declassifiers f:int→τf and g:int→τg for some τf and τg, we use type variable αf,g as the type for x and use αf,g→τf and αf,g→τg as types for xf and xg.
To support policies where multiple inputs can be declassified via a declassifier, e.g. inputs x and y can be declassified via f=λz:int×int.(π1z+π2z)/2, we introduce a new term variable z which is corresponding to a tuple of two inputs x and y and we require that only z can be declassified. The type of z is αf and two tuples ⟨v1,v2⟩ and ⟨v1′,v2′⟩ are indistinguishable at αf when f ⟨v1,v2⟩=f ⟨v1′,v2′⟩.
5 Related Work
.
Typing secure information flow.
Pottier and Simonet [35] implement FlowCaml [36],
the first type system for information flow analysis dealing with a real-sized programming language (a large fragment of OCaml), and they prove soundness. In comparison with our results, we do not consider any imperative features;
they do not consider any form of declassification,
their type system significantly departs from ML typing, and their security proof is not based on an abstraction theorem.
An interesting question is whether their type system can be
translated to system F or some other calculus with an abstraction theorem.
FlowCaml provides type inference for security types.
Our work relies on the Standard ML type system to enforce security.
Standard ML provides type inference, which endows our approach with an inference mechanism.
Barthe et al. [9] propose a modular method to reuse type systems and proofs for noninterference [43] for declassification. They also provide a method to conclude declassification soundness by using an existing noninterference theorem [40].
In contrast to our work, their type system significantly departs from standard typing rules, and does not make use of parametricity.
Tse and Zdancewic [50] propose a security-typed language for robust declassification: declassification cannot be triggered unless there is a digital certificate to assert the proper authority.
Their language inherits many features from System F*<:* and uses monadic labels as in DCC [1].
In contrast to our work, security labels are based on the Decentralized Label Model (DLM) [30], and are not semantically unified with the standard safety types of the language.
The Dependency Core Calculus (DCC) [1] expresses security policies using monadic types
indexed on levels in a security lattice with the usual interpretation that flows are only allowed between levels in accordance with the ordering.
DCC does not include declassification and the noninterference theorem of [1] is proved from scratch (not leveraging parametricity).
While DCC is a theoretical calculus, its monadic types fit nicely with the monads and monad transformers used by the Haskell language for computational effects like state and I/O.
Algehed and Russo [5] encode the typing judgment of DCC in Haskell
using closed type families, one of the type system extensions supported by GHC that brings it close to dependent types.
However, they do not prove security.
Compared with type systems, relational logics can specify IF policy and prove more programs secure through semantic reasoning [31, 8, 24, 10],
but at the cost of more user guidance and less familiar notations.
Aguirre et al [2] use relational higher order logic to prove soundness of DCC essentially by formalizing the semantics of DCC [1].
Connections between secure IF and type abstraction.
Tse and Zdancewic [49] translate the recursion-free fragment of DCC to System F.
The main theorem for this translation aims to show that parametricity of System F implies noninterference.
Shikuma and Igarashi identify a mistake in the proof [44]; they
also give a noninterference-preserving translation for a version of DCC to the simply-typed lambda calculus.
Although they make direct use of a specific logical relation,
their results are not obtained by instantiating a parametricity theorem.
Bowman and Ahmed [12] finally provide a translation from
the recursion-free fragment of DCC to System Fω, proving that parametricity implies noninterference,
via a correctness theorem for the translation (which is akin to a full abstraction property).
Bowman and Ahmed’s translation makes essential use of the power of System Fω to encode judgments of DCC.
Algehed and Bernardy [4] translate a label-polymorphic variant DCC (without recursion) into the calculus of constructions (CC) and prove noninterference directly from a parametricity result for CC [11].
The authors note that it is not obvious this can be extended to languages with nontermination or other effects.
Their results have been checked in Agda and the presentation achieves elegance owing to the fact that
parametricity and noninterference can be explicitly defined in dependent type theory; indeed, CC terms can represent proof of parametricity [11].
Our goals do not necessitate a system like DCC for policy,
raising the question of whether a simpler target type system can suffice for security policies expressed differently from DCC.
We answer the question in the affirmative, and believe our results for polymorphic lambda (and for ML) provide transparent explication of noninterference by reduction to parametricity.
The preceding works on DCC are “translating noninterference to parametricity” in the sense of translating both programs and types.
The implication is that one might leverage an existing type checker by translating both a program and its security policy into another program such that it’s typability implies the original conforms to policy.
Our work aims to cater more directly for practical application, by minimizing the need to translate the program and hence avoiding the need to prove the correctness of a translation.
Cruz et al. [17] show that type abstraction implies relaxed noninterference.
Similar to ours, their definition of relaxed noninterference is a standard extensional semantics, using partial equivalence relations.
This is in contrast with Li and Zdancewic [27] where the semantics is entangled with typability.
Protzenko et al. [37] propose to use abstract types as the types for secrets and use standard type systems for security.
This is very close in spirit to our work.
Their soundness theorem is about a property called “secret independence”, very close to noninterference.
In contrast to our work, there is no declassification and no use of the abstraction theorem.
Rajani and Garg [38] connect fine- and coarse-grained type systems for information flow in a lambda calculus with general references, defining noninterference (without declassification) as a step-indexed Kripke logical relation that expresses indistinguishability.
Further afield, a connection between security and parametricity is made
by Devriese et al [18], featuring a negative result:
System F cannot be compiled to the the Sumii-Pierce calculus of dynamic sealing [47]
(an idealized model of a cryptographic mechanism).
Finally, information flow analyses have also been put at the service of parametricity [54].
Abstraction theorems for other languages.
Parametricity remains an active area of study [46].
Vytiniotis and Weirich [52] prove the abstraction theorem for Rω, which extends Fω with constructs that are useful for programming with type equivalence propositions.
Rossberg et al [41] show another path to parametricity for ML modules, by translating them to Fω.
Crary’s result [14] covers a large fragment of ML but without references and mutable state.
Abstraction theorems have been given for mutable state,
based on ownership types [6]
and on more semantically based reasoning [3, 20, 7, 48].
6 Discussion and Conclusion
In this work, we show how to express declassification policies by using standard types
of the simply typed lambda calculus.
By means of parametricity, we prove that type checking implies relaxed noninterference,
showing a direct connection between declassification and parametricity.
Our approach should be applicable to other languages that have an abstraction theorem (e.g [7, 3, 20, 48]) with the potential benefit of strong security assurance from off-the-shelf type checkers.
In particular, we demonstrate (in an appendix) that the results can be extended to a large fragment of ML including general recursion.
Although in this paper we demonstrate our results using confidentiality and declassification, our approach applies as well to integrity
and endorsement, as they have been shown to be information flow properties analog to confidentiality [26, 23, 21, 22].
The simple encodings in the preceding sections do not support computation and output at multiple levels.
For example, consider a policy where x is a confidential input that can be declassified via f and we also want to do the computation x+1 of which the result is at confidential level.
Clearly, x+1 is ill-typed in the public interface.
We provide (in an appendix) more involved encodings supporting computation at multiple levels.
To have an encoding that support multiple levels, we add universally quantified types ∀α.τ to the language presented in §2.
However, this goes against our goal of minimizing complexity of translation.
Observe that many applications are composed of programs which, individually, do not output at multiple levels; for example, the password checker, and data mining computations using sensitive inputs to calculate aggregate or statistical information. For these the simpler encoding suffices.
Vanhoef et al. [51] and others have proposed more expressive declassification policies than the ones in Li and Zdancewic [27]: policies that keep state and can be written as programs. We speculate that TRNI for stateful declassification policies
can be obtained for free in a language with state—indeed, our work provides motivation for
development of abstraction theorems for such languages.
Acknowledgements.
We thank anonymous reviewers for their suggestions. This work was partially supported by CISC ANR-17-CE25-0014-01, IPL SPAI, the European Union’s Horizon 2020 research and innovation programme under grant agreement No 830892,
and US NSF award CNS 1718713.
Contents of appendix
§0.A describes extensions for more expressive policies,
in terms of the encoding in §4.
§0.B is an overview of our results for the ML module calculus
and §0.C is an overview of our encoding for computation at multiple security levels.
§0.D provides proofs for §2
and §0.E provides proofs for §4.
The following sections present the ML encoding (§0.F–§0.H)
and the multi-level encoding (§0.I–§0.J)
in detail.
Appendix 0.A Extensions
The extensions in this section are corresponding to the encoding in §4.
0.A.1 Declassification policies
Variations of our encoding can support richer declassification policies and accept more secure programs.
We consider two ways to extend our encoding.
More declassification functions.
The notation in [27] labels an input with a set of declassification functions,
so in general an input can be declassified in more than one way.
To show how this can be accomodated,
we present an extension for a policy P where VP={x}, and x can be declassified via f or g for some f and g, where ⊢f:int→τf and ⊢g:int→τg.
The confidential view and the public view for this policy are as below:
[TABLE]
We now have a new definition of indistinguishability.
The definition is similar to the one presented in §4, except that we add a new rule for αf,g.
{mathpar}
\inferrule∗[left=Eq−Var4]⊢v1,v2:int⟨f v1,f v2⟩∈IE[[τf]]⟨g v1,g v2⟩∈IE[[τg]]⟨v1,v2⟩∈IV[[αf,g]]
With the new encoding and the new definition of indistinguishability, we can define TRNI(P,τ) as in Definition 3.
From the abstraction theorem, we again obtain that for any program e, if ΓCP⊢e, and ΔPP,ΓPP⊢e:τ, then e is TRNI(P,τ).
For example, we consider programs e1=xf x and e2=xg x.
These two programs are well-typed in both views of P, and in the public view, their types are respectively τf and τg.
Thus, e1 is TRNI(P,τf), and e2 is TRNI(P,τg).
Using an equivalent function to declassify.
In most type systems for declassification, the declassifier function or expression must be identical to the one in the policy.
Indeed, policy is typically expressed by writing a “declassify” annotation on the expression [42].
However, the type system presented in [27, § 5] is more permissive:
it accepts a declassification if it is semantically equivalent to the policy function, according to
a given syntactically defined approximation of equivalence.
Verification tools can go even further in reasoning with semantic equivalence [31, 24],
but any automated checker is limited due to undecidability of semantic equivalence.
We consider a policy P where there are two confidential inputs x and y, x can be declassified via f, and y can be declassified via g, f:int→τ, and g:int→τ for some τ.
Suppose that there exists a function a s.t. f∘a=g semantically.
With the encoding in §4, we accept g y, or rather xg y, but we cannot accept f(a y)
even though it is semantically the same.
To accept programs like f(a y), based on the idea of the first extension, we encode the policy as below, where y is viewed as a confidential input that can be declassified via g or f∘a.
Note that in the following encoding, we have two type variables: αg,f∘a for the confidential input, and αf for the result of xa x which can be declassified via f.
[TABLE]
Indistinguishability for this policy is defined similarly to the one in Section 4, except that we have the following rule for αg,f∘a.
{mathpar}
\inferrule∗[left=Eq−Var6]⊢v1:int⊢v2:int⟨g v1,g v2⟩∈IE[[τ]]⟨v1,v2⟩∈IV[[αg,f∘a]]
As in the first extension, we can define TRNI for a type τ well-formed in ΔPP and we have the free theorem stating that if ΓCP⊢e, and ΔPP,ΓPP⊢e:τ, then e is TRNI(P,τ).
W.r.t. the new encoding, both yg y and xf(xa y) are well-typed in the public view.
In other words, we accepts both yg y and xf(xa y).
Notice that as discussed in [27], the problem of establishing relations between declassification functions in general is undecidable. Thus, the relations should be provided or can be found in a predefined amount of time. Otherwise, the relations are not used in the encoding and programs like xf(ya y) will not typecheck.
0.A.2 Global policies
The policies considered in §4 and §0.A.1 are corresponding to local policies in [27].
We now consider policies where a declassifier can involve more than one confidential input.
To be consistent with [27], we call such policies global policies.
For simplicity, in this subsection, we consider a policy P where there are two confidential inputs, x1 and x2, which can be declassified via f of the type int1×int2→τf.555We can extend the encoding presented in this section to have policies where different subsets of VP can be declassified and to have more than one declassifier associated with a set of confidential inputs.
Notice that here we use subscripts for the input type of f to mean that the confidential input xi is corresponding to i-th element of an input of f.
Example 8 (Average can be declassified)
We consider the policy PAve where there are two confidential inputs x1 and x2 and their average can be declassified.
That is x1 and x2 can be declassified via f=λx:int×int.(π1x+π2x)/2.
In our encoding, we need to maintain the correspondence between inputs and arguments of the declassifier since we want to prevent laundering attacks [42].
A laundering attack occurs, for example, when the declassifier f is applied to ⟨x1,x1⟩,
since then the value of x1 is leaked.
In the general case, to encode the requirement that a specific n-tuple of confidential inputs can be declassified via f, we introduce a new variable y.
The basic idea is that y is corresponding to that n-tuple of confidential inputs, xi cannot be declassified, and only y can be declassified via f.
Therefore, the confidential and public views are as below,
where for readability we show the case n=2.
[TABLE]
For each i∈{1,…,n}, since xi cannot be declassified, the indisinguishability for αxi is the same as the one for αx described in Fig. 3.
Since y corresponds to the tuple of confidential inputs and only it can be declassified via f, indistinguishability for the type of y in the public view αf is as below (again, case n=2).
[TABLE]
We next encode the correspondence between inputs and argument of the declassifier.
We say that a term substitution γ is consistent w.r.t. ΓPP if γ⊨δP(ΓPP) and in addition, for all i∈{1,2}, πi(γ(y))=γ(xi).
As we can see, the additional condition takes care of the correspondence of inputs and the arguments of the intended declassifier.
We next define the type substitution and indistinguishable term substitutions for P.
We say that δP⊨ΔPP when δP(αf)=int×int and for all αxi, δP(αxi)=int.
We say that two term substitutions γ1 and γ2 are indistinguishable w.r.t. P (denoted by ⟨γ1,γ2⟩∈IV[[P]]) if γ1 and γ2 are consistent w.r.t. ΓPP,
γ1(yf)=γ2(yf)=f,
for all other x∈dom(ΓPP), ⟨γ1(x),γ2(x)⟩∈IV[[ΓPP(x)]].
Then we can define TRNI(P,τ) as in Def. 3 (except that we use the new definition of indistinguishable term substitutions). We also have the free theorem stating that if e has no type variable and ΔPP,ΓPP⊢e:τ, then e is TRNI(P,τ). The proof goes through without changes.
Example 9 (Average can be declassified - cont.)
Here we present the encoding for the policy PAve described in Example 8.
The confidential and public views for this policy is as below:
[TABLE]
We can easily check that the program yf y is TRNI(PAve,int); it is well-typed in both views, and in the public view its type is int.
Appendix 0.B TRNI for Module Calculus: summary
This section recapitulates the development of §4 but using an encoding suited to the module calculus
of Crary and Dreyer [19, 14].666Our only change is to add int and arithmetic primitives, for examples.
It is a core calculus that models Standard ML including higher order generative and applicative functors, sharing constraints (via singleton kinds), and sealing. Sealing ascribes a signature to a module expression and thereby enforces data abstraction.
The syntax is in Fig. 4.
The calculus has static expressions: kinds (k), constructors (c) and signatures (σ), and dynamic expressions: terms (e) and modules (M).
The full formal system is given in §0.F; here we sketch highlights.
The unit kind 1 has only the unit constructor ⋆.
The base kind, T, is for types that can be used to classify terms.
By convention, we use the metavariable τ for constructors that are types (i.e. of the kind T).
The singleton kind S(c) classifies constructors that are definitionally equivalent to c.
In addition, we have higher kinds: dependent functions Πα:k1.k2 and dependent pairs Σα:k1.k2.
The syntax for terms is standard and includes general recursion (fixτe).
Module expressions include unit module (⋆),
pairing/projection,
atomic modules with a single static or dynamic component ((∣c∣), ⟨∣e∣⟩),
generative and applicative functors (λgnα/m:σ.M, λapα/m:σ.M,
the applications of which are written resp. M1 M2, M1⋅M2),
and unpacking (unpack[α,x]=e in (M:σ)).
While term binding is as usual (let x=e in M),
the module binding construct is unusual: let α/m=M1 in (M2:σ) binds a pair of names,
where constructor variable α is used to refer to the static part of M1 (and m to the full module).
This is used to handle the phase distinction between compile-time and run-time expressions.
A signature describes an interface for a module.
Signatures include unit signature, atomic kind and atomic type signature,
generative and applicative functors, and dependent pairs (Σα:σ1.σ2).
A signature σ is transparent when it exposes the implementation of the static part of modules of σ.
A signature σ is opaque when it hides some information about the static part of modules of σ.
The sealing construct, M:>σ, ascribes a signature to the module in the sense of enforcing σ as an abstraction boundary.
Abstraction theorem.
The static semantics includes judgments
⊢Γ ok,
Γ⊢e:τ, Γ⊢PM:σ, and Γ⊢IM:σ for resp. well-formed context, well-typed term, pure well-formed module, and impure well-formed module.
The pure and impure judgment forms roughly correspond to unsealed and sealed modules; the formal system treats sealing as an effect, introduced by application of a generative functor as well as by the sealing construct.
The dynamic semantics is call-by value, with these values:
[TABLE]
The logical relation for the calculus is more complicated than the one in §2.
Even so, the statement of the abstraction theorem for terms is similar to the one in §2.
Theorem 0.B.1 (Abstraction theorem [14])
Suppose that ⊢Γok.
If Γ⊢e:τ, then Γ⊢e∼e:τ.
Modules and terms are interdependent, and Crary’s theorem
includes corresponding results for pure and for impure modules.
We express security in terms of sealed modules, but our security proof only relies on the abstraction theorem for expressions.
Free theorem: TRNI for the module calculus.
We present the idea of the encoding for the module calculus.
(Formalization of the encoding can be found in §0.G.)
To make the presentation easier to follow, in this section, we write examples in Standard ML (SML).
These examples are checked with SML of New Jersey, version 110.96 [45].
For a policy P, we construct the public view and the confidential view by using signatures containing type information of confidential inputs and their associated declassifiers.
In particular, the signature for the confidential view is a transparent signature which exposes the concrete type of confidential input, while the signature for the public view is an opaque one which hides the type information of confidential inputs.
For example, for the policy POE (see Example 1), we have the following signatures, where transOE and opaqOE are respectively the transparent signature for the confidential view and the opaque signature for the public view.
[TABLE]
Different from §4, a program has only a module input which is of the transparent signature and contains all confidential inputs and their declassifiers. A program can use the input via the module variable m.
For example, for POE, we have the program m.f m.x, which is corresponding to the program xf x in Example 5.
Using the result in §4, we define indistinguishability
as an instantation of the logical relation,
and we say that a term e is TRNI(P,τ) if on indistinguishable substitutions w.r.t. P, it generates indistinguishable outputs at τ.
By using the abstraction theorem 0.B.1 for terms, we obtain our main result.
Theorem 0.B.2
If the type of e in the public view is τ, then e is TRNI(P,τ).
For the module calculus, when e is well-typed in the public view, e is also well-typed in the confidential view.
Therefore, different from Theorem 4.1 which requires that e has no type variable, Theorem 0.B.2 simply requires that e is well-typed in the public view.
Our example program m.f m.x typechecks at int,
so by Theorem 0.B.2 it is TRNI(POE,int).
Usage of our approach.
We can use our approach with ordinary ML implementations.
In the case that the source programs are already parameterized by one module for their confidential inputs and their declassifiers, then there is no need to modify source programs at all.
For example, we consider program described below.
Here M is a module of the transparent signature transOE. By sealing this module with the opaque signature opaqOE, we get the module opaqM.
Intuitively, program is TRNI(POE,int) since the declassifier f is applied to the confidential input x.
We also come to the same conclusion from the fact that the type of this program is int.
⬇
structure M = struct
type t = int
val x : t = 1
val f : t -> int = fn x => x mod 2
end
structure opaqM :> opaqOE = M
val program : int = opaqM.f opaqM.x
So far our discussion is about open terms but the ML type checker only applies to closed terms.
In the case that the client program is open
(i.e. that it can receive any module of the transparent signature as an input, as in the program m.f m.x presented above), in order to be able to type check it for a policy, we need to close it
by putting in a closing context, which we call wrapper.
For any program e and policy P,
the wrapper is written using a functor as shown below, where
opaqP is the opaque signature for the public view of P.
Type τ is the type at which we want to check security of e.
(The identifiers program and wrapper are arbitrary.)
⬇
functor wrapper (structure m: opaqP) =
struct
**val** program : $\tau$ = $e$
end
Note that e is unchanged.
We have proved that if the wrapper wrapP(e)
is of the signature from opaqP to τ, then the type of e in the public view is τ.
Therefore, from Theorem 0.B.2, e is TRNI at τ.
For instance, for the policy POE, we have that wrapP(m.f m.x) is of the signature from transOE to int and hence, we infer that the type of m.f m.x in the public view is int and hence, m.f m.x is TRNI(POE,int).
Extension.
As in the case of the simple calculus, our encoding for ML can also be extended for policies where multiple inputs are declassified via a declassifier.
Here, for illustration purpose, we present the encoding for a policy which is inspired by two-factor authentication.
Example 10
The policy PAut involves two confidential passwords and two declassifiers checking1 and checking2 as below, where input1 and input2 are respectively the first input and the second input from a user.
Notice that checking2 takes a tuple of two passwords as its input.
⬇
fun checking1(password1:int) =
if (password1 = input1) then 1 else 0
fun checking2(passwords:int*int) =
if ((#1 passwords) = input1) then
**if** ((#2 passwords) = input2) **then** 1 **else** 0
else 2
We next construct the confidential view and the public view for the policy.
To encode the requirement that two passwords can be declassified via checking2, we introduce a new variable passwords which is corresponding to the tuple of the two passwords, and only passwords can be declassified via checking2.
The transparent signature for the confidential view of PAut is below.
⬇
signature transAut = sig
type t1 = int
val password1:t1
val checking1:t1->int
type t2 = int
val password2:t2
type t3 = int * int
val passwords:t3
val checking2:t3 ->int
end
The signature opaqAut for the public view is the same except
the types t1, t2, and t3 are opaque.
We have that the programs m.checking2 m.passwords and m.checking1 m.password1, where m is a module variable of the transparent signature transAut, have the type int in the public view. Hence both programs are TRNI(PAut,int).
Appendix 0.C Computation at multiple security levels: summary
The encodings in the preceding sections do not support computation and output at multiple levels.
For example, consider a policy where x is a confidential input that can be declassified via f and we also want to do the computation x+1 of which the result is at confidential level.
Clearly, x+1 is ill-typed in the public interface.
To support computation at multiple levels we develop a monadic encoding inspired by DCC,
and a public interface that represents policy for multiple levels.
To have an encoding that support multiple levels, we add universally quantified types ∀α.τ to the language presented in §2 (already present in ML).
In addition, to simplify the encoding, we add the unit type unit.
W.r.t. these new types, we have new values: the unit value ⟨⟩ of unit, and values Λα.e of ∀α.τ.
To facilitate the presentation of the idea of the encoding, we consider a lattice L with three different levels L, M, H such that L⊏M⊏H.
We also use a simple policy P with three inputs hi, mi and li at resp. H, M and L, and hi can be declassified via f:int→int to M.
(The encoding with an arbitrary finite lattice and policy is in §0.I.)
For simplicity, we suppose that values on input and output channels are of int type.
To model multiple outputs we consider programs that return a tuple of values, one component for each output channel.
To model channel access being associated with different security levels, the output values
are wrapped, in the form λx:unit.n.
To read such a value, an observer needs to provide an appropriate key.
By giving x an abstract type corresponding to a security level, we can control access.
Similar to the previous sections, we assume that free variables in programs are their inputs,
but now the values will be wrapped integers.
Intuitively, a wrapped value v can be unwrapped by unwrap k v, where k is an appropriate key, and unwrap k v can be implemented as the application of v on k (i.e. v k).
Concretely, k will be the unit value ⟨⟩.
We further assume that programs are executed in a context where there are several output channels, each corresponding to a security level.
A program will compute a tuple of wrapped values, where each element of the output tuple can be unwrapped by using an appropriate key and the unwrapped value is sent to the channel.
In short, we assume the program of interest is executed in a context that wraps its inputs, and also
unwraps each components of the output tuple and sends the value on the corresponding channel.
This assumption is illustrated in the following pseudo program, where e is the program of interest, o is the computed tuple, Output.Channell is an output channel at l, kl is a key to unwrap value at l, and πl projects the output value for the output channel l.
⬇
let o = e in
Output.ChannelL := unwrap kL (πL o)
Output.ChannelM := unwrap kM (πM o)
Output.ChannelH := unwrap kH (πH o)
The keys are not made directly available to e, which must manipulate its inputs via an interface described below.
Encoding.
Different from the previous sections, we use type variables αH,αM and αL as the types of keys for unwrapping wrapped values at H, M and L. This idea is similar to the idea in [27]. Different from [27], we do not translate DCC and we support declassification.
For an input at l that cannot be declassified (mi or li), its type in the public view is αl→int.
For the input hi which can be declassified via f, we use another type variable (i.e. αHf) as the type of key to unwrapped values.777If we use αH instead, since this input can be declassified to M, the indistinguishability will be incorrect: all wrapped values at H are wrongly indistinguishable to observer M.
Similar to the previous sections, we use αf to encode number values at H.
Therefore, the type of hi in the public view is αHf→αf.
As we use unit as the type for key,
in the confidential view the type of hi, mi, and li is unit→int.
As assumed above, a program computes an output which is a tuple of three wrapped values.
Since we use type variables as keys to unwrap wrapped values, the type of outputs of programs we consider is (αH→int)×(αM→int)×(αL→int).
To support computing outputs at a level l, by using the idea of monad, we have interfaces cpl and wrl which are the bind and unit expressions for a monad.
In addition, to support converting a wrapped value at l to l′ (where l⊏l′), we have interfaces cvull′.
To use hi in a computation at H, we have cvf.
Similar to the previous sections, we have hif for the declassfier f.
The types of there interfaces are described in Fig. 5.
Example 11
We illustrate the idea of the encoding by writing a program that computes the triple hi+li+1, f hi and li+1 at resp. H, M, and L.
First, we will have e1 that does the computation at L: li+1.
Let plus_one=λx:int.x+1.
In order to use cpL, we first wrap plus_one by using wrL.
[TABLE]
Then e1 is as below:
[TABLE]
Next, we have e2 that does the computation hi+li at H.
Let add be a function of the type int→int→int.
From add, we construct wrap_addc of the type int→αH→int,
where c is a variable of the type int.
[TABLE]
Then we have e2 as below.
Note that in order to use li in cpH, we need to convert li from level L to level H by using cvuLH.
[TABLE]
At this point, we can write the program e that computes hi+li+1, f hi, and li+1 at resp. H, M, and L.
[TABLE]
The implementations of the defined interfaces are straightforward.
For example, on a protected input of type unit→β1 and a continuation of type β1→(unit→β2), the implementation comp of cpl first unfolds the protected input by applying it to the key ⟨⟩ and then applies the continuation on the result.
[TABLE]
The implementation of wrl is Λβ.λx:β.λ_:unit.x.
The conversions cvull′ are implemented by the identity function.
Indistinguishability.
Different from §4, indistinguishability is defined for observer ζ (ζ∈L). 888Following [12], we use ζ for observers.
The indistinguishability relations for ζ at type τ on values (denoted as IPζ[[τ]]) is defined as an instance of the logical relation with a careful choice of interpretations for αl and αHf.
The idea is that if the observer ζ cannot observe data at l (i.e. l⊑ζ), ζ does not have any key to unwrap these values and hence, all wrapped values at l are indistinguishable to ζ. Thus, αl is interpreted as the empty relation for ζ.
Otherwise, since ζ has key and can unwrapped values, values wrapped at l are indistinguishable to ζ if they are equal and hence, αl is interpreted as {⟨⟨⟩,⟨⟩⟩} (note that the concrete type for key is unit).
Since wrapped numbers from hi are indistinguishable to observer ζ when they cannot be distinguish by the declassifier f, the interpretation of αHf for the observer M is
{⟨⟨⟩,⟨⟩⟩}.999Therefore, if we used αH→αf for hi, all wrapped values from hi would be indistinguishable to the observer M since this observer do not have any key to open data at H that cannot be declassified (to observer M, the interpretation of αH is empty.
By using the idea in the previous sections, based on IPζ[[τ]], we define indistinguishability relations for ζ at type τ on terms (denoted as IPζ[[τ]]ev)).
Free theorem.
We write ρ as an environment that maps type variables to its interpretations of form ⟨τ1,τ2,R⟩ and maps term variables to tuples of values.
(This is similar to the formalization for §0.G.)
We write ρL and ρR for the mappings that map every variable in the domain of ρ to respectively the first element and the second element of the tuple that ρ maps that variable to.
The application of ρL (resp. ρR) to e is denoted by ρL(e) (resp. ρR(e)) (this notations is similar to δγ(e) in §2).
We write ρ⊨ζfullP to mean that ρ maps inputs to tuples of indistinguishable values.
By leveraging the abstraction theorem, we get the free theorem saying that a well-typed program e maps indistinguishable inputs to indistinguishable outputs.
Theorem 0.C.1
If ΔP,ΓP⊢e:τ, then for any ζ∈L and ρ⊨ζfullP,
[TABLE]
We state it this way to avoid spelling out the definition of TRNI for this encoding.
The encoding presented here can also be extended to support richer policies described in Remark 1.
Remark 2
Our encoding supports declassification while DCC does not.
However, if we consider programs without declassification then DCC is more expressive since in our encoding, to use a wrapped value in a computation at l, this value must be wrapped at l′ such that l′⊑l.
However, in DCC, this is not the case due to the definition of the “protected at” judgment in DCC: if type τ is already protected at l then so is Tl′τ for any l′.
Therefore, data protected at l can be used in a computation protected at l′ even when l′⊑l.
For example, we consider the encoding for a policy defined in a lattice with four levels ⊤, M1, M2, ⊥ where ⊤⊏Mi⊏⊤ but M1 and M2 are incomparable.
We can have the following well-typed program in DCC (the program is written in the notations in [12]).
[TABLE]
In our encoding, this program can be rewritten as below, where f:int→αM2→αM1→int is from function λy:int.y+1 (see a similar function in Example 11).
[TABLE]
This program is not well-typed in our encoding.
This feature of DCC, allowing multiple layers of wrapping, is needed to encode state-passing programs (in particular, to encode the Volpano-Smith system for while programs) where low data is maintained unchanged through high computations. The feature seems unnecessary for functional programs.
Appendix 0.D Proofs of Section 2
Lemma 1.
Suppose that ρ∈Rel(δ1,δ2) for some δ1 and δ2.
For i∈{1,2}, it follows that:
if ⟨v1,v2⟩∈[[τ]]ρ, then ⊢vi:δi(τ), and
if ⟨e1,e2⟩∈[[τ]]ρev, then ⊢ei:δi(τ).
Proof
The second part of the lemma follows directly from rule FR-Term.
We prove the first part of the lemma by induction on structure of τ.
Case 1: int.
We consider ⟨v1,v2⟩∈[[int]]ρ.
From FR-Int, we have that ⊢vi:int.
Since δi(int)=int, we have that ⊢vi:δ(int).
Case 2: α.
We consider ⟨v1,v2⟩∈[[α]]ρ.
From the FR-Var rule, ⟨v1,v2⟩∈ρ(α)∈Rel(δ1(α),δ2(α)).
From the definition of Rel(δ1(α),δ2(α)), we have that ⊢vi:δi(α).
Case 3: τ1×τ2.
We consider ⟨v1,v2⟩∈[[τ1×τ2]]ρ.
We then have that v1=⟨v11,v12⟩ for some v11 and v12 and v2=⟨v21,v22⟩ for some v21 and v22.
From FR-Pair, it follows that ⟨v11,v21⟩∈[[τ1]]ρ and ⟨v12,v22⟩∈[[τ2]]ρ.
From IH (on τ1 and τ2), we have that ⊢v11:δ1(τ1), ⊢v21:δ2(τ1), ⊢v12:δ1(τ2), and ⊢v22:δ2(τ2).
From FT-Pair, ⊢⟨v11,v12⟩:δ1(τ1)×δ1(τ2) and ⊢⟨v21,v22⟩:δ2(τ1)×δ2(τ2).
Thus, ⊢v1:δ1(τ1)×δ1(τ2) and ⊢v2:δ2(τ1)×δ2(τ2).
In other words, ⊢v1:δ1(τ1×τ2) and ⊢v2:δ2(τ1×τ2).
Case 4: τ1→τ2.
We consider ⟨v1,v2⟩∈[[τ1→τ2]]ρ.
We now look at arbitrary ⟨v1′,v2′⟩∈[[τ1]]ρ.
From FR-Fun, it follows that ⟨v1v1′,v2v2′⟩∈[[τ2]]ρev.
From IH on τ1 and the second part of the lemma on τ2, we have that ⊢vi′:δi(τ1) and ⊢vivi′:δi(τ2) (for i∈{1,2}).
From FT-App, we have that ⊢vi:δi(τ1→τ2).
Theorem 2.1.
If Δ,Γ⊢e:τ, then Δ,Γ⊢e∼e:τ.
Proof
We prove the theorem by induction on typing derivation.
Case 1: Rule FT-Int.
[TABLE]
From FR-Int, we have that ⟨n,n⟩∈[[int]]ρ.
Therefore, from FR-Term, it follows that ⟨n,n⟩∈[[int]]ρev.
Hence, ⟨δ1γ1(n),δ2γ2(n)⟩∈[[int]]ρev.
The proof is closed for this case.
Case 2: Rule FT-Var.
[TABLE]
Since ⟨γ1,γ2⟩∈[[Γ]]ρ and x∈dom(γ1)=dom(γ2), we have that ⟨γ1(x),γ2(x)⟩∈[[Γ(x)]]ρ, and hence ⟨γ1(x),γ2(x)⟩∈[[Γ(x)]]ρev.
Since there is no type variable in x, we have that δ1γ1(x)=γ1(x) and δ2γ2(x)=γ2(x).
As proven above, ⟨γ1(x),γ2(x)⟩∈[[τ]]ρev.
Thus, we have that ⟨δ1γ1(x),δ2γ2(x)⟩∈[[τ]]ρev.
The proof is closed for this case.
Case 3: Rule FT-Pair.
[TABLE]
From IH, it follows that
⟨δ1γ1(e1),δ2γ2(e1)⟩∈[[τ1]]ρev, and
⟨δ1γ1(e2),δ2γ2(e2)⟩∈[[τ2]]ρev.
From the FR-Term, we have that
⟨v11,v12⟩∈[[τ1]]ρ, where ⟨δ1γ1(e1),δ2γ2(e1)⟩\rightarrowtriangle∗⟨v11,v12⟩, and
⟨v21,v22⟩∈[[τ2]]ρ, where ⟨δ1γ1(e2),δ2γ2(e2)⟩\rightarrowtriangle∗⟨v21,v22⟩.
From FR-Pair, it follows that ⟨⟨v11,v21⟩,⟨v12,v22⟩⟩∈[[τ1×τ2]]ρ.
From FR-Term, we have that
[TABLE]
Thus, ⟨δ1γ1⟨e1,e2⟩,δ2γ2⟨e1,e2⟩⟩∈[[τ1×τ2]]ρev.
This case is closed.
Case 4: rule FT-Prj.
[TABLE]
From IH, we have that ⟨δ1γ1(e),δ2γ2(e)⟩∈[[τ1×τ2]]ρev.
Thus, ⟨⟨v11,v21⟩,⟨v12,v22⟩⟩∈[[τ1×τ2]]ρ, where δ1γ1(e)\rightarrowtriangle∗⟨v11,v21⟩ and δ2γ2(e)\rightarrowtriangle∗⟨v12,v22⟩.
From FR-Pair, we have that ⟨v11,v12⟩∈[[τ1]]ρ and ⟨v21,v22⟩∈[[τ2]]ρ.
Since δ1γ1(e)\rightarrowtriangle∗⟨v11,v21⟩ and δ2γ2(e)\rightarrowtriangle∗⟨v12,v22⟩
π1δ1γ1(e)\rightarrowtriangle∗v11,
π2δ1γ1(e)\rightarrowtriangle∗v12,
π1δ2γ2(e)\rightarrowtriangle∗v12,
π2δ2γ2(e)\rightarrowtriangle∗v22.
Thus,
δ1γ1(π1e)\rightarrowtriangle∗v11,
δ1γ1(π2e)\rightarrowtriangle∗v12,
δ2γ2(π1e)\rightarrowtriangle∗v12,
δ2γ2(π2e)\rightarrowtriangle∗v22.
Thus,
⟨δ1γ1(π1e),δ2γ2(π1e)⟩\rightarrowtriangle∗⟨v11,v12⟩ and
⟨δ1γ1(π2e),δ2γ2(π2e)⟩\rightarrowtriangle∗⟨v12,v22⟩.
As proven above ⟨v11,v12⟩∈[[τ1]]ρ and ⟨v21,v22⟩∈[[τ2]]ρ.
From FR-Term, we have that ⟨δ1γ1(π1e),δ2γ2(π1e)⟩∈[[τ1]]ρev and ⟨δ1γ1(π2e),δ2γ2(π2e)⟩∈[[τ2]]ρev.
This case is closed.
Case 5: rule FT-Fun.
[TABLE]
From IH, we have that ⟨δ1γ1[x↦v1](e),δ2γ2[x↦v2](e)⟩∈[[τ2]]ρev, where ⟨v1,v2⟩∈[[τ1]]ρev.
Hence, we have that ⟨δ1γ1(e[x↦v1]),δ2γ2(e[x↦v2])⟩∈[[τ2]]ρev.
From the semantics of the language and the FR-Term rule, it follows that
[TABLE]
Since ⟨v1,v2⟩ are arbitrary, from FR-Fun, we have that ⟨δ1γ1(λx:τ1.e),δ2γ2(λx:τ1.e)⟩∈[[τ1→τ2]]ρ, and hence ⟨δ1γ1(λx:τ1.e),δ2γ2(λx:τ1.e)⟩∈[[τ1→τ2]]ρev.
The proof is closed for this case.
Case 6: rule FT-App.
[TABLE]
The proof follows from IH and rule FR-Fun.
Appendix 0.E Proofs of Section 4
Lemma 2.
ρP∈Rel(δP,δP).
Proof
We need to prove that for any type variable α, if ⟨v1,v2⟩∈ρP(α), then ⊢vi:δP(α) and hence ⊢vi:int
according to the definition (1).
This follows directly from the definition of ρP and rules Eq-Var1, Eq-Var2, and Eq-Var3.
Lemma 5
Suppose that ⊢v:τ
It follows that:
if τ is int, v is n for some n**,
if τ is τ1→τ2, v is λx:τ1.e for some e**,
if τ is τ1×τ2, it is ⟨v1,v2⟩ for some v1 and v2**.
Proof
We prove the case of int first by case analysis on typing rules.
The FT-Int rule gives us the desired result.
The other rules cannot be instantiated with an expression that is a value and of the int type.
We prove the case of τ1→τ2 by case analysis on typing rules.
The FT-Fun rule gives us the desired result.
The other rules cannot be instantiated with an expression that is a value and of the τ1→τ2 type.
The proof for the case τ1×τ2 is similar.
Lemma 3.
It follows that
⟨v1,v2⟩∈[[τ]]ρP iff ⟨v1,v2⟩∈IV[[τ]], and
⟨e1,e2⟩∈[[τ]]ρPev iff ⟨e1,e2⟩∈IE[[τ]].
Proof
We prove the lemma by induction on the structure of τ.
Case 1: int.
We consider IV[[int]] and [[int]]ρP
We have that ⟨n,n⟩∈[[int]]ρP iff ⟨n,n⟩∈IV[[int]].
We consider IE[[int]] and [[int]]ρPev.
We consider ⟨e1,e2⟩.
If ⟨e1,e2⟩∈IV[[int]], from Eq-Term and Eq-Int, there exists n s.t. ei\rightarrowtriangle∗n.
From FR-Int and FR-Term, ⟨e1,e2⟩∈[[int]]ρPev.
If ⟨e1,e2⟩∈[[int]]ρPev, from FR-Term and FR-Int, there exists n s.t. ei\rightarrowtriangle∗n.
From Eq-Int and Eq-Term, ⟨e1,e2⟩∈IE[[int]].
Case 2: αx.
First we consider IV[[αx]] and [[αx]]ρP.
From the definition of ρP and the FR-Var rule, ⟨v1,v2⟩∈[[αx]]ρP iff ⟨v1,v2⟩∈IV[[αx]].
Case 3: αf.
The proof is similar to the one of Case 2.
Case 4: τ1×τ2.
We first consider IV[[τ1×τ2]] and [[τ1×τ2]]ρP.
Suppose that ⟨v1,v2⟩∈IV[[τ1×τ2]].
From the definition of indistinguishability, we have that ⊢vi:δP(τ1×τ2).
From Lemma 5, v1=⟨v11,v12⟩ and v2=⟨v21,v22⟩.
Thus, we have that
⟨⟨v11,v12⟩,⟨v21,v22⟩⟩∈IV[[τ1×τ2]].
From the Eq-Pair rule, we have that ⟨v11,v21⟩∈IV[[τ1]] and ⟨v12,v22⟩∈IV[[τ2]].
From IH on τ1 and τ2, we have that ⟨v11,v21⟩∈[[τ1]]ρP and ⟨v12,v22⟩∈[[τ2]]ρP.
From the FR-Pair, it follows that ⟨⟨v11,v12⟩,⟨v21,v22⟩⟩∈[[τ1×τ2]]ρP.
Suppose that ⟨v1,v2⟩∈[[τ1×τ2]]ρP.
From Lemma 1, ⊢vi:δP(τ1×τ2).
Thus, we have that ⟨⟨v11,v12⟩,⟨v21,v22⟩⟩∈[[τ1×τ2]]ρP.
From the FR-Pair rule, we have that ⟨v11,v21⟩∈[[τ1]]ρP and ⟨v12,v22⟩∈[[τ2]]ρP.
From IH on τ1 and τ2, we have that ⟨v11,v21⟩∈IV[[τ1]] and ⟨v12,v22⟩∈IV[[τ2]].
From the Eq-Pair, it follows that ⟨⟨v11,v12⟩,⟨v21,v22⟩⟩∈IV[[τ1×τ2]].
We now consider IE[[τ1×τ2]] and [[τ1×τ2]]ρPev.
Suppose that ⟨e1,e2⟩∈IE[[τ1×τ2]].
From Eq-Term, we have that ei\rightarrowtriangle∗vi for some vi and ⟨v1,v2⟩∈IV[[τ1×τ2]].
As proven above, we have that ⟨v1,v2⟩∈[[τ1×τ2]]ρP.
From FR-Term, ⟨e1,e2⟩∈[[τ1×τ2]]ρPev.
Suppose that ⟨e1,e2⟩∈[[τ1×τ2]]ρPev.
From FR-Term, we have that ei\rightarrowtriangle∗vi for some vi and ⟨v1,v2⟩∈[[τ1×τ2]]ρP.
As proven above, we have that ⟨v1,v2⟩∈IV[[τ1×τ2]].
From Eq-Term, ⟨e1,e2⟩∈IE[[τ1×τ2]].
Case 5: τ1→τ2.
We first consider IV[[τ1→τ2]] and [[τ1→τ2]]ρP.
Suppose ⟨v1,v2⟩∈IV[[τ1→τ2]].
We need to prove that for any ⟨v1′,v2′⟩∈[[τ1]]ρP, ⟨v1v1′,v2v2′⟩∈[[τ2]]ρPev.
Since ⟨v1′,v2′⟩∈[[τ1]]ρP, from IH on τ1, we have that ⟨v1′,v2′⟩∈IV[[τ1]].
Since ⟨v1,v2⟩∈IV[[τ1→τ2]], from Eq-Fun, we have that ⟨v1 v1′,v2 v2′⟩∈IE[[τ2]].
From IH on τ2, ⟨v1 v1′,v2 v2′⟩∈[[τ2]]ρPev.
Suppose that ⟨v1,v2⟩∈[[τ1→τ2]]ρP.
We need to prove that for any ⟨v1′,v2′⟩∈IV[[τ1]], ⟨v1v1′,v2v2′⟩∈IE[[τ2]].
Since ⟨v1′,v2′⟩∈IV[[τ1]], from IH on τ1, we have that ⟨v1′,v2′⟩∈[[τ1]]ρP.
Since ⟨v1,v2⟩∈[[τ1→τ2]]ρP, from Eq-Fun, we have that ⟨v1 v1′,v2 v2′⟩∈[[τ2]]ρPev.
From IH on τ2, ⟨v1 v1′,v2 v2′⟩∈IE[[τ2]].
We now consider IE[[τ1→τ2]] and [[τ1→τ2]]ρPev.
Suppose that ⟨e1,e2⟩∈IE[[τ1→τ2]].
From Eq-Term, ei\rightarrowtriangle∗vi for some vi and ⟨v1,v2⟩∈IV[[τ1→τ2]].
As proven above, we have that ⟨v1,v2⟩∈[[τ1→τ2]]ρP.
Thus, ⟨e1,e2⟩∈[[τ1→τ2]]ρPev.
Suppose that ⟨e1,e2⟩∈[[τ1→τ2]]ρPev.
From FR-Term, ei\rightarrowtriangle∗vi for some vi and ⟨v1,v2⟩∈[[τ1→τ2]]ρP.
As proven above, we have that ⟨v1,v2⟩∈IV[[τ1→τ2]].
Thus, ⟨e1,e2⟩∈IE[[τ1→τ2]].
Lemma 4.
If ⟨γ1,γ2⟩∈IV[[P]], then ⟨γ1,γ2⟩∈[[ΓPP]]ρP.
Proof
We first prove that dom(γ1)=dom(γ2)=dom(ΓPP).
This is directly from the definition of ⟨γ1,γ2⟩∈IV[[P]].
We now need to prove that ⟨γ1(x),γ2(x)⟩∈[[ΓPP]]ρP for all x.
From the construction of ΓPP, we have the following cases.
Case 1: ΓPP(x)=αx.
From the assumption, we have that
[TABLE]
From Lemma 3, it follows that ⟨γ1(x),γ2(x)⟩∈[[αx]]ρP.
Case 2: ΓPP(x)=αf
From the assumption, we have that
[TABLE]
From Lemma 3, it follows that ⟨γ1(x),γ2(x)⟩∈[[αf]]ρP.
Case 3: ΓPP(xf)=αf→τ.
We need to prove that ⟨f,f⟩∈[[αf→τ]]ρP, where ⊢f:int→τ for some τ s.t. ⊢τ.
From FR-Fun, we need to prove that for any ⟨v1,v2⟩∈[[αf]]ρP, ⟨f v1,f v2⟩∈[[τ]]ρPev.
We consider an arbitrary ⟨v1,v2⟩∈[[αf]]ρP.
From the Eq-Var2 rule, we have that ⟨f v1,f v2⟩∈IE[[τ]].
From Lemma 3, ⟨f v1,f v2⟩∈[[τ]]ρPev.
Case 4: ΓPP(xa)=αf∘a→αf.
We need to prove that ⟨a,a⟩∈[[αf∘a→αf]]ρP, where ⊢a:int→int.
From FR-Fun, we need to prove that for any ⟨v1,v2⟩∈[[αf∘a]]ρP, ⟨a v1,a v2⟩∈[[αf]]ρPev.
We consider an arbitrary ⟨v1,v2⟩∈[[αf∘a]]ρP.
From the Eq-Var3 rule, we have that ⟨a v1,a v2⟩∈IE[[αf]].
From Lemma 3, ⟨a v1,a v2⟩∈[[αf]]ρPev.
Appendix 0.F Module Calculus
0.F.1 Syntax and semantics
This section presents a module calculus, essentially the same as that of Crary [14] except that we add int for integers.
Crary’s calculus is adapted from Dreyer’s thesis [19], and
the reader should consult these references for explanations and motivation.
As described in §0.B, the calculus has static expressions: kinds (k), constructors (c) and signatures (σ), and dynamic expressions: terms (e) and modules (M).
The syntax is in Fig. 4.
Kinds and constructors.
The unit kind 1 has only the unit constructor ⋆.
The kind T have base types that can be used to classify terms.
The singleton kind S(c) (where c is of the base kind) has constructors that are definitionally equivalent to c.
In addition, we have higher kinds: dependent functions Πα:k1.k2 and dependent pairs Σα:k1.k2.
A constructor c of the kind Σα:k1.k2 has pairs of constructors where the first component π1c is of the kind k1 and the second component π2c is of the kind k2[α↦π1c].
A constructor c of the kind Πα:k1.k2 takes a constructor c′ of kind k1 as a parameter and returns a constructor of the kind k2[α↦c′].
When α does not appear free in k2, we write k1→k2 instead of Πα:k1.k2 and k1×k2 instead of Σα:k1.k2.
We use the metavariable τ for constructors that are types (i.e. of the kind T).
Terms and modules.
The syntax for terms is standard.
Modules can be unit module, static atomic module, dynamic atomic module, generative functor, applicative functor, application, pair, projection, unpack, term binding, module binding, and sealing.
Applications of generative functors and applicative functors are syntactically distinguished.
Abstraction is introduced by sealing: in the module M:>σ, access to the component M is limited to the interface σ.
A term is extracted from a module ⟨∣e∣⟩ by Ext ⟨∣e∣⟩.
To extract the static part of a module, we have the operation Γ⊢Fst(M)≫c meaning that the static part of M is c in Γ.
When the context is empty, we write Fst(M) for c where ⊢Fst(M)≫c.
Notice that every module variable is associated with a constructor variable that represents its static part [14].
The relation is maintained by twinned variables: α/m:σ meaning that m has signature σ and its static part is α which is of the kind Fst(σ), where for any signature σ, Fst(σ) extracts the information about kind from σ.
Whenever m:σ and Fst(m)≫c, it follows that c is of the kind Fst(σ).
Signature.
Signatures include unit signature, atomic kind signature, atomic type signature, signatures for generative functors, applicative functors and pairs.
Since a module does not appear in static part of a signature, we have only α in dependent signatures (instead of twinned variables, e.g. α/m, as in the case of modules).
In the binding α:σ within a dependent signature, α corresponds to the static part of some module of the signature σ.
Thus, α has the kind Fst(σ).
As described in [19], a signature σ is transparent when it exposes the implementation of the static part of modules of σ.
A signature σ is opaque when it hides some information about the static part of modules of σ.
Example 12
We consider the following module and signatures.
Suppose that f=λx:int.e for some e which is a closed function of the type int→τf for some closed τf.
[TABLE]
In the module calculus, M is ⟨(∣int∣),⟨⟨∣0∣⟩,⟨∣λx:int.e∣⟩⟩⟩.
Using abbreviations,
σT is ⟨(∣S(int)∣),⟨⟨∣int∣⟩,⟨∣int→τf∣⟩⟩⟩
and σO is
Σα:(∣T∣).⟨⟨∣α∣⟩,⟨∣α→τf∣⟩⟩.101010Expanding abbreviations,
σT is Σα:(∣S(int)∣).Σβ:⟨∣int∣⟩.⟨∣int→τf∣⟩ and
σO is Σα:(∣T∣).Σβ:⟨∣α∣⟩.⟨∣α→τf∣⟩.
The signature σT is a transparent signature of M since σT exposes the information of the static part of M,
as (∣S(int)∣).
The signature σO is an opaque signature of M since σO hides the information of the static part of M,
as (∣T∣).
Static semantics.
The judgment forms in the static semantics are described in Figure 8.
W.r.t. the static semantics, for the signatures described in Example 12, it follows that the transparent signature σT is a sub-signature of the opaque signature σO.
Example 13 (Opaque signature)
We consider a module M=⟨(∣int∣),⟨∣0∣⟩⟩ and show that it has the opaque signature σO=Σα:(∣T∣).⟨∣α∣⟩
111111Notice that in Example 12, we have M=⟨(∣int∣),⟨⟨∣0∣⟩,⟨∣λx:int.e∣⟩⟩⟩ and σO=Σα:(∣T∣).Σβ:⟨∣α∣⟩.⟨∣α→τf∣⟩. From the static semantics, we can also derive that ⊢PM:σO. Here, to simplify the presentation, we have M=⟨(∣int∣),⟨∣0∣⟩⟩ and σO=Σα:(∣T∣).⟨∣α∣⟩.
We then have that M is a pure module of the signature σO (i.e. ⊢PM:σO).
First, we have that M is a module of a transparent signature, i.e. ⊢PM:Σα:(∣S(int)∣).⟨∣int∣⟩ by instantiating the ofm_pair rule.
[TABLE]
Next, we have that ⊢Σα:(∣S(int)∣).⟨∣int∣⟩≤Σα:(∣T∣).⟨∣α∣⟩, by the derivation described in Fig. 20:
Finally, it follows that ⊢PM:σO.
[TABLE]
From [14], we have the following lemma about the correctness of Fst(M)≫c operation.
Lemma 6
If Γ⊢PM:σ then Γ⊢Fst(M)≫c and Γ⊢c:Fst(σ).
To facilitate the proofs about TRNI for ML, from the static semantics, we have the following lemma.
Lemma 7 (Weakening)
Suppose that ⊢Γ,α:k ok.
It follows that:
if Γ⊢σ:sig, then Γ,α:k⊢σ:sig,
if Γ⊢c:k′, then Γ,α:k⊢c:k′,
if Γ⊢k′:kind, then Γ,α:k⊢k′:kind,
if Γ⊢k1≡k2:kind, then Γ,α:k⊢k1≡k2:kind,
if Γ⊢k1≤k2:kind, then Γ,α:k⊢k1≤k2:kind,
if Γ⊢c1≡c2:k′, then Γ,α:k⊢c1≡c2:k′.
Proof
We prove this lemma by induction on the derivation of Γ⊢σ:sig, Γ⊢c:k′, Γ⊢k′:kind, Γ⊢k1≡k2:kind, Γ⊢k1≤k2:kind, and Γ⊢c1≡c2:k′.
Dynamic semantics.
The dynamic semantics is given by call-by value semantics.
We have dynamic semantics for terms Γ⊢e\rightarrowtrianglee′ and for modules Γ⊢M\rightarrowtriangleM′ (see Fig. 21 and Fig. 22), where
the context Γ is only used to extract the static part of module values.
Open term values and module values are as below.
[TABLE]
In the tstep_fix rule, λ_:unit.fixτe means that the term variable bound by λ is a fresh variable.
To be precise, the variable must not be in dom(Γ), and in addition it should be canonically chosen, to maintain strict determinacy of evaluation. In Crary’s deBruin representation this is automatic.
We use V,W as metavariables for module values.
We write e↓ when the evaluation of e terminates.
Similarly, we have M↓.
0.F.2 Logical relation
In order to define logical relation, we define some auxiliary notions as in [14]
Given a relation R∈Rel(τ,τ′), Rs contains continuations that agree on values related by R.
Conversely, given a relation S on continuations, related continuations by S agree on terms in St.
From _s and _t, we define Pitts closed relations.
Definition 4 (Closure)
For R∈Rel(τ,τ′), define
[TABLE]
For S∈Rel(τ→unit,τ′→unit), define
St≜{⟨w:τ,w′:τ⟩ ∣ ∀⟨v,v′⟩∈S,vw↓⇔v′w′↓}.
For R∈Rel(τ,τ′), define
[TABLE]
Relation R∈Rel(τ,τ′) is Pitts closed if R=Rst.
We have similar definitions for relations defined on closed signatures σ1 and σ2, where the signatures for continuations are Πgnα:σ1.1 and Πgnα:σ2.1,
which can be abbreviated as σ1→1 and σ2→1.
Apropos the stev closure, we may be able to infer indirectly that two terms are related by Rstev when these two terms depend on terms related by Qstev.
Definition 5
Suppose x:ϱ⊢e:τ.
We say that x is active in e if for all closed e′ s.t. ⊢e′:ϱ, e[x↦e′]↓ implies e′↓.
Lemma 8
Suppose Q∈Rel(ϱ1,ϱ2), R∈Rel(τ1,τ2), x:ϱi⊢ei:τi, and x is active in e1 and e2.
If for all ⟨v1,v2⟩∈Q, ⟨e1[x↦v1],e2[x↦v2]⟩∈Rstev, then
[TABLE]
From [14] and Lemma wf_mr in [15], we have the following lemma about properties of logical interpretations of constructors, kinds and signatures.
Lemma 9
Suppose that ⊢Γ ok and ⟨ρ,ρ′⟩∈[[Γ]]. Then
If Γ⊢c:k, then ⟨ρL(c),ρR(c),[[c]]ρ,[[c]]ρ′⟩∈[[k]]ρ.
If Γ⊢k1≡k2, then [[k1]]ρ=[[k2]]ρ
If Γ⊢σ:sig, then [[σ]]ρ=[[σ]]ρ′.
If Γ⊢σ≡σ′:sig, then [[σ]]ρ=[[σ′]]ρ.
Precandiate.
As in [14], we next present simple kinds which are used in the definitions of logical interpretations of dependent kinds.
A simple kind is a kind that does not have singleton kinds.
Given a kind k, simp(k) returns a simple kind by replacing singleton kinds in k with T.
A candidate of a kind is a pre-candidate which is in an interpretation of a kind.
We use Q as a meta-variable for pre-candidates in general, Φ for pre-candidates over function kinds, P for pre-candidates over pair kinds, and R for pre-candidates over T.
[TABLE]
Logical interpretations for kinds and constructors.
Following [14], we generalize ρ presented in §2 to a mapping that maps constructor variables to tuples of the form ⟨c,c′,Q⟩, term variables to tuples of the form ⟨v,v′⟩, and module variables to tuples of the form ⟨V,V′⟩.
Notice that in the simple language, for any α∈dom(ρ), ρ(α)=R∈Rel(τ1,τ2) for some τ1 and τ2.
If we use the notation in this section, then we have that ρ(α)=⟨τ1,τ2,R⟩.
We write ρL and ρR for the substitutions that map every variable in the domain of ρ to respectively the first element and the second element of the tuple that ρ maps that variable to.
If we do not have module variables, then, ρL(_) is similar to δ1γ1(_) and ρR(_) is similar to δ2γ2(_) in §2, where δ1 and δ2 are type substitutions in ρ, and γ1 and γ2 are term substitutions in ρ.
Logical interpretations for kinds and constructors are presented in Fig. 23
121212The presentation of logical interpretations here is similar to the one in [14]. Notice that we can write definitions of logical interpretations in the form of inference rules as in §2..
The interpretation of a kind k is a tuple ⟨c,c′,Q,Q′⟩ where c and c′ are closed constructors of the kind k, and Q and Q′ are candidates relating c and c′.
Notice that since pre-candidates are defined only for simple kinds, in the logical interpretations of Πα:k1.k2 and Σα:k1.k2, we use respectively PreCandsimp(Πα:k1.k2) and PreCandsimp(Σα:k1.k2).
In addition, in the definition for Πα:k1.k2, since Φ and Φ′ are pre-candidates of simp(Πα:k1.k2), we require that Q and Q′ are pre-candidates of simp(k1)
131313Notice that from definition of PreCandΠα:k1.k2, we have that Φ⟨d,d′,Q⟩ and Φ⟨d′′,d′′′,Q′⟩ are in PreCandsimp(k2)..
The definitions for types of T (e.g. τ1→τ2) are similar to the ones of the simple language.
Logical interpretations for signatures.
Logical interpretations for signatures are presented in Fig. 24.
The logical interpretation of a signature σ of modules is a set of ⟨V1,V2,Q⟩ where the dynamic values in V1 and V2 are related at their types, and the static part (constructors) are related by Q.
For example, we consider the signature Σα:(∣k∣).⟨∣τ∣⟩.
The logical interpretation of this signature with a ρ is a set of ⟨⟨V1,V1′⟩,⟨V2,V2′⟩,⟨P,P′⟩⟩ where (1) V1=(∣c∣), V2=(∣c′∣) for some c and c′ s.t. ⟨c,c′,P,P⟩∈[[k]]η; and (2) V2=⟨∣v∣⟩, V2′=⟨∣v′∣⟩ for some v and v′ s.t. ⟨v,v′⟩∈[[τ]]ρ (from the definition of [[⟨∣τ∣⟩]]ρ we also know that P′=⟨⟩).
Definition 6
We say that ⟨ρ,ρ′⟩∈[[Γ]] if whenever Γ(α)=k, there exists ρ(α)=⟨c1,c2,Q⟩ and ρ′(α)=⟨c1′,c2′,Q′⟩ s.t. ⊢c1≡c1′:ρL(k), ⊢c2≡c2′:ρR(k), and ⟨c1,c2,Q,Q′⟩∈[[k]]ρ,
We say that ρ∈[[Γ]]full if ⟨ρ,ρ⟩∈[[Γ]] and
for all x:τ∈Γ, there exists ρ(x)=⟨v1,v2⟩ s.t. ⟨v1,v2⟩∈[[τ]]ρ,
for all α/m:σ∈Γ, there exists ρ(m)=⟨V1,V2⟩ and ρ(α)=⟨Fst(V1),Fst(V2),Q⟩ s.t. ⟨V1,V2,Q⟩∈[[σ]]ρ.
Terms e and e′ are logically equivalent at τ in Γ (written as Γ⊢e∼e′:τ) if ⊢Γ ok implies Γ⊢e,e′:τ, and for all ρ∈[[Γ]]full, ⟨ρL(e),ρR(e′)⟩∈[[τ]]ρev.
Notice that equivalence holds vacuously, if Γ is not well formed, but we are never interested in such Γ.
Theorem 0.F.1 (Abstraction theorem)
Suppose that ⊢Γok.
If Γ⊢e:τ, then Γ⊢e∼e:τ.
In [14], there are similar results for pure modules and impure modules. Later we express security in terms of sealed modules, but our security proof only relies on the abstraction theorem for expressions.
Appendix 0.G TRNI for the Module Calculus
This section recapitulates the development of §4 but using an encoding suited to the module calculus.
The free theorem that typing implies security (Theorem 0.B.2) is
formulated for an open term in context of the public view, as in Theorem 4.1.
We then develop a “wrapper” to encapsulate the typing problem in a closed form.
That could facilitate use of an unmodified ML compiler without recourse to an API for the typechecker.
0.G.1 Declassification policy encoding
In this section, we present the encoding for declassification policies by using the module calculus.
Here, a declassification function can be written in the module calculus with recursive functions.
However, for simplicity and for coherent policy, we assume—as in §3—that the applications of declassifiers on confidential input values always terminate.
In §4, a view is a typing context that declares variables for inputs and for declassifiers.
Here, those are gathered in a signature and the view is a context that declares a module of that signature.
Let L⊆VP be a finite list of distinct confidential input variables from VP.
An empty list is []. We write x::L to concatenate a confidential input variable to L.
In §4 we define operations ⟨⟨−⟩⟩C and ⟨⟨−⟩⟩P that
apply to policy variables and declasifiers, yielding the encoding of policy as typing contexts. Here we use the same notation, but apply the operations to variable lists
and encode policy as signatures.
First, we define ⟨⟨L⟩⟩C to return a transparent signature of the policy.
It is defined inductively as described in Fig. 25.
As in §4, we use fresh constructor variables with names that indicate their role in the encoding.
For a confidential input x, basically, the signature is a pair containing information about the kind of its type, its type, and the types of associated declassifiers.
For example, for x that can be declassified via f, the signature contains: (1) the kind of the type of x: (∣S(int)∣), (2) the type of x: ⟨∣int∣⟩, and (3) the type of f: ⟨∣int→τf∣⟩.
Example 14 (Transparent signature)
For POE (Example 1), since f=λx:int.xmod2 is of the type int→int, by applying the third case in ⟨⟨−⟩⟩C with τf=int, we get the signature
[TABLE]
that can be abbreviated as ⟨(∣S(int)∣),⟨⟨∣int∣⟩,⟨⟨∣int→int∣⟩,1⟩⟩⟩.
In ML it looks like
[TABLE]
We overload ⟨⟨L⟩⟩P to get an opaque signature of the policy.
The idea is similar to ⟨⟨L⟩⟩C, except that here we use constructor variables of the T kind for types of confidential inputs and in types of declassification functions.
The definition is described in Fig. 25.
Example 15 (Opaque signature)
For POE (Example 1), since f=λx:int.xmod2 is of the type int→int, by applying the third case in ⟨⟨−⟩⟩P with τf=int, we get the signature
[TABLE]
that can be abbreviated as Σαf:(∣T∣).⟨⟨∣αf∣⟩,⟨⟨∣αf→int∣⟩,1⟩⟩.
In ML it looks like sig type t val x:t val f: t->int end.
Hereafter, we abuse VP and use it as a list and we write σPC and σP to mean respectively ⟨⟨VP⟩⟩C and ⟨⟨VP⟩⟩P.
In order to define TRNI, we define the confidential view and the public view as in §4.
The confidential view is based on the constructed transparent signature σPC,
and the public view is based on the constructed opaque signature σP.
[TABLE]
To express what in Example 2 and Example 3
(for POE) is written xfx,
in the module calculus x is accessed as Ext(π1(π2mPOE)) and xf is accessed as Ext(π1(π2(π2mPOE))).
From the definitions, we have that σPC and σP are closed and well-formed signatures,
and σPC is a subsignature of σP.
0.G.2 TRNI
In order to define an environment ρ for the policy, we define relations Rx and Rf
similar to the relations IV[[αx]] and IV[[αf]] in §4.
[TABLE]
Notice that ∅ in [[τ]]∅ev is the empty environment.
Given a list L of confidential inputs from P and an environment ρ, we say that ρ∈∣L∣P when
ρ maps mP in ΓPP to related module values V1 and V2 for some V1 and V2 s.t. V1 and V2 are of the transparent signature ⟨⟨VP⟩⟩C and functions in V1 and V2 are declassification functions from the policy, and
the confidential values in V1 and V2 are related by Rx, Rf, or Rf∘a according to the policy, and
ρ maps αP to a tuple ⟨c1,c2,Q⟩ where c1 and c2 are static parts from respectively V1 and V2, and Q depends on the policy.
That is if an element in Q is corresponding to an αx:(∣T∣), then this element is Rx, if an element in Q is corresponding to an αf:(∣T∣), then this element is Rf, and if an element in Q is corresponding to an αf∘a:(∣T∣), then this element is Rf∘a.
The definition of ρ∈∣L∣P is as below.
Hereafter, we write {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\rho\models^{\mathsf{full}}\mathcal{P}}} when ρ∈∣VP∣P.
Definition 7 (full environments for P)
Given L⊆VP, we define the set ∣L∣P of environments by
ρ∈∣L∣P iff dom(ρ)={αP,mP} and
if L=[] then
ρ(mP)=⟨⋆,⋆⟩ and
ρ(αP)=⟨⋆,⋆,⟨⟩⟩,
if L=x::L′ and x∈dom(FP) then
there are ⟨v1,v2⟩∈Rx and ρ′∈∣L′∣P with
[TABLE]
where ρ′(mP)=⟨V1′,V2′⟩ and ρ′(αP)=⟨c1′,c2′,Q′⟩,
if L=x::L′ and FP(x)=f then there are ⟨v1,v2⟩∈Rf and ρ′∈∣L′∣P with
[TABLE]
where ρ′(mP)=⟨V1′,V2′⟩ and ρ′(αP)=⟨c1′,c2′,Q′⟩.
Example 16 (ρ⊨fullPOE)
In this example, we present a full environment for POE.
We first define Rf, where f=λx:int.xmod2.
[TABLE]
Following the definition of ρ⊨fullPOE, we construct ρ as below. Notice that ⟨2,4⟩∈Rf.
[TABLE]
It follows that ρ⊨fullPOE.
Next we prove that if τ is a type in the public view ΓPP, then all its logical interpretations are the same.
Lemma 10
If ρ1⊨fullP, ρ2⊨fullP, and ΓPP⊢τ:T, then [[τ]]ρ1=[[τ]]ρ2.
Therefore, we define indistinguishability based on an arbitrary ρ⊨fullP.
Definition 8 (Indistinguishability)
Suppose ρ and τ satisfy ρ⊨fullP and ΓPP⊢τ:T.
Values v1 and v2 are indistinguishable at τ (written as ⟨v1,v2⟩∈IV[[τ]]) if ⟨v1,v2⟩∈[[τ]]ρ.
Terms e1 and e2 are indistinguishable at τ (written as ⟨e1,e2⟩∈IE[[τ]]) if ⟨e1,e2⟩∈[[τ]]ρev.
Example 17 (Indistinguishability)
We consider POE (Example 1).
As described in Example 15, the opaque signature of the policy is σPOE=Σαf:(∣T∣).Σα1:⟨∣αf∣⟩.Σα2:⟨∣αf→int∣⟩.1.
Thus, the public view ΓPPOE is αPOE/mPOE:σPOE.
Notice that since αPOE and mPOE are twinned, it follows that αPOE is of the kind Fst(σP)=Σαf:T.Σα1:1.Σα2:1.1.
We consider the type π1αPOE.
By a rule for well-formed constructors (rule ofc_pi1), we have that ΓPPOE⊢π1αPOE:T.
Thus, we can define indistinguishability for this type.
As presented in Example 16, ρ⊨fullPOE.
Therefore, we have that IV[[π1αPOE]]=[[π1αPOE]]ρ=Rf (the definition of Rf is in Example 16).
Next, we define TRNI for the module calculus.
The definition here is similar to the one in §4.
Definition 9 (TRNI for the module calculus)
A term e is TRNI(P,τ) if ΓCP⊢e, and ΓPP⊢τ:T, and for all ρ⊨fullP, it follows that ⟨ρL(e),ρR(e)⟩∈IE[[τ]].
Example 18
We consider the program e=(\textsf{Ext(\pi_{1}(\pi_{2}(\pi_{2}m_{\mathcal{P}{\textit{OE}}})))})\ (\textsf{Ext(\pi{1}(\pi_{2}m_{\mathcal{P}_{\textit{OE}}}))}), which is corresponding to the program xf x in Example 6,
as noted following Eqn. (2).
We now check e with the definition of TRNI.
We consider an arbitrary ρ⊨fullPOE.
As described in Example 16, ρ is as below, where ⟨v1,v2⟩∈Rf.
[TABLE]
We have that ρL(e)=f v1=v1mod2 and ρR(e)=f v2=v2mod2.
Since ⟨v1,v2⟩∈Rf, we have that (v1mod2)=int(v2mod2). Thus, ⟨ρL(e),ρR(e)⟩∈[[int]]ρev.
In other words, ⟨ρL(e),ρR(e)⟩∈IE[[int]].
Therefore, e is TRNI(POE,int).
0.G.3 Free theorem: typing in the public view implies security
To apply the abstraction theorem to get the free theorem, we need
the following.
Lemma 11
Suppose that ρ⊨fullP.
It follows that ρ∈[[ΓPP]]full.
Lemma 12
If ΓPP⊢e:τ, then ΓCP⊢e.
Theorem 0.B.2.
If ΓPP⊢e:τ, then e is TRNI(P,τ).
Proof
Since ΓPP⊢e:τ, from Theorem 0.F.1, we have that ΓPP⊢e∼e:τ.
Thus, for any ρ∈[[ΓPP]]full, it follows that:
[TABLE]
We consider an arbitrary ρ s.t. ρ⊨fullP.
From Lemma 11, it follows that ρ∈[[ΓPP]]full.
As proven above, we have that ⟨ρL(e),ρR(e)⟩∈[[τ]]ρev.
From the definition of indistinguishability, we have that ⟨ρL(e),ρR(e)⟩∈IE[[τ]].
In addition, since ΓPP⊢e:τ, from Lemma 12, it follows that ΓCP⊢e.
Therefore, e is TRNI(P,τ).
Example 19 (Typing implies TRNI)
We consider the policy POE. As described in Example 14 and Example 15, the transparent signature and the opaque signature of the policy are as below.
[TABLE]
Thus, the confidential view is ΓCPOE=αPOE/mPOE:σPOEC, and the public view is ΓPPOE=αPOE/mPOE:σPOE.
We now look at the program e=e1 e2, where e_{1}=(\textsf{Ext(\pi_{1}(\pi_{2}(\pi_{2}m_{\mathcal{P}{\textit{OE}}})))}) and e_{2}=(\textsf{Ext(\pi{1}(\pi_{2}m_{\mathcal{P}_{\textit{OE}}}))}).
This program is corresponding to the program xf x in Example 6,
as noted following definition (2).
We have that ΓCPOE⊢e1:int→int, ΓCPOE⊢e2:int, ΓPPOE⊢e1:π1αPOE→int, and ΓPPOE⊢e2:π1αPOE.
Therefore, we have that ΓCPOE⊢e:int, and ΓPPOE⊢e:int and hence, from Theorem 0.B.2, the program is TRNI(POE,int).
Example 20
The purpose of this example is similar to the one of Example 7: to illustrate that if a program is well-typed in the confidential view and is not TRNI(P,τ) for some τ well-formed in the public view, then the type of the program in the public view is not equivalent to τ or the program is not well-typed in the public view.
We consider the policy POE and the program Ext(π1(π2mPOE)), which is corresponding to the program x in Example 7.
This program is not TRNI(POE,int) since Ext(π1(π2mPOE)) itself is
confidential and cannot be directly declassified. In the public view of the policy, the type of this program is π1αPOE which is not equivalent to int.
We consider another program: e=(\textsf{Ext(\pi_{1}(\pi_{2}m_{\mathcal{P}_{\textit{OE}}}))})\mathbin{\mathit{mod}}3, which is corresponding to the program xmod3 in Example 7.
This program is not TRNI(POE,π1αPOE) since it may map indistinguishable inputs to non-indistinguishable outputs.
For example, we consider ρ⊨fullPOE presented in Example 17.
We have that ρL(e)=2mod3=2, and ρR(e)=4mod3=1.
As described in Example 17, IV[[π1αPOE]]=Rf={⟨v1,v2⟩ ∣ (v1mod2)=int(v2mod2)}.
Therefore ⟨1,2⟩∈IV[[π1αPOE]].
As explained above, e is not TRNI(POE,π1αPOE).
In the public view, it is not well-typed since the type of Ext(π1(π2mPOE)) is π1αPOE, which is not equivalent to int, and mod expects int arguments.
0.G.4 Wrapper
In this section, we will transform an open term to a closed module.
We then prove that if the closed module is well-typed in the empty context, then the original open term is well-typed in the public view and hence, e is TRNI.
Thus we can use our approach with ordinary ML implementations.
If the source programs are already parameterized by one module for their confidential inputs and their declassification functions, then there is no need to modify source programs at all.
We next define a wrapper that wraps e with the information from the public view.
[TABLE]
From the construction, we have that if wrapP(e) is well-typed in the empty context, then the original term is also well-typed in the public view.
In addition, we can infer the type of the original term in the public view.
These results yield, by Theorem 0.B.2,
that the original term is TRNI when the wrapper is well-typed.
Theorem 0.G.1
If ⊢PwrapP(e):ΠgnαP:σP.⟨∣τ∣⟩, then e is TRNI(P,τ).
Example 21
In this example, we combine the ideas presented in §0.A.2, §0.G.1, and §0.G.4 to encode a complex policy which is inspired by two-factor authentication.
The policy PAut involves two confidential passwords and two declassifiers checking1 and checking2 written in SML as below, where input1 and input2 are respectively the first input and the second input from a user.
Notice that checking2 takes a tuple of two passwords as its input.
⬇
fun checking1(password1:int) =
if (password1 = input1) then 1 else 0
fun checking2(passwords:int*int) =
if ((#1 passwords) = input1) then
**if** ((#2 passwords) = input2) **then** 1 **else** 0
else 2
Using the ideas presented in §0.A.2, we introduce a new variable which corresponding to the tuple of two passwords.
The confidential and public signatures of PAut in the module calculus are as below, where f1 and f2 are corresponding to checking1 and checking2.
[TABLE]
The confidential and public signatures of PAut in SML are as below.
⬇
signature traSIG=sig
type t1 = int
val password1:t1
val checking1:t1->int
type t2 = int
val password2:t2
type t3 = int * int
val passwords:t3
val checking2:t3 ->int
end
⬇
signature opaSIG=sig
type t1
val password1:t1
val checking1:t1->int
type t2
val password2:t2
type t3
val passwords:t3
val checking2:t3->int
end
As in §0.A.2, we require that for ρ⊨fullPAut, ρL and ρR are consistent.
That is when ρL(mPAut)=VL, then VL.passwords=⟨VL.password1,VL.password2⟩ (and we have a similar requirement for ρR).
In order to define indistinguishability for PAut, we need to define
ρ⊨fullPAut,141414Notice that as noted in the main text, ρL and ρR are consistent.
and hence, we define Rf1, Rx2, Rf2 as below.
[TABLE]
By using the wrapper presented above, we can check that programs
[TABLE]
and mPAut.checking1 mPAut.password1
are TRNI(PAut,int), where mPAut is the module variable in confidential and public views of PAut.
Remark 3 (On wrapper)
We may choose an applicative functor for wrapping the original program. However, w.r.t. this choice, we need to handle more cases in proofs.
Thus, we choose a generative functor.
Appendix 0.H Proofs for TRNI for the Module Calculus
0.H.1 Properties of the encoding
Lemma 13
For any L⊆VP, it follows that ⊢⟨⟨L⟩⟩C:sig.
Proof
We prove the lemma by induction on L.
We have four cases.
Case 1: L=[].
We have that ⟨⟨VP⟩⟩C=1.
From the ofs_one rule, it follows that ⊢1:sig.
Case 2: L=x::L′, x∈dom(FP).
We have that ⟨⟨L⟩⟩C=Σαx:(∣S(int)∣).Σα:⟨∣int∣⟩.⟨⟨L′⟩⟩C.
From IH, we have that ⊢⟨⟨L′⟩⟩C:sig.
Thus, we have the following derivation.
Notice that Fst(⟨∣c∣⟩)=1 for any c and Fst((∣S(int)∣))=S(int)
[TABLE]
Case 3: L=x::L′, FP(x)=f, where ⊢f:int→τ.
We have that ⟨⟨L⟩⟩C=Σαf:(∣S(int)∣).Σα1:⟨∣int∣⟩.Σα2:⟨∣int→τ∣⟩.⟨⟨L′⟩⟩C.
We now look at Σα2:⟨∣int→τ∣⟩.⟨⟨L′⟩⟩C.
Notice that since ⊢f:int→τ, we have that ⊢int→τ:T.
From the ofs_dyn rule, ⊢⟨∣int→τ∣⟩:sig.
Thus, we have that:
[TABLE]
In addition, by using a reasoning similar to the one in Case 2, we have:
⊢(∣S(int)∣):sig,
αf:S(int)⊢⟨∣int∣⟩:sig.
Therefore, we have that:
[TABLE]
Lemma 14
For any L⊆VP, it follows that ⊢⟨⟨L⟩⟩P:sig.
Proof
We prove the lemma by induction on L.
We have four cases.
Case 1: L=[].
We have that ⟨⟨L⟩⟩P=1.
From the ofs_one rule, we have that ⊢1:sig.
Case 2: L=x::L′, x∈dom(FP).
We have that ⟨⟨L⟩⟩P=Σαx:(∣T∣).Σα:⟨∣αx∣⟩.⟨⟨L′⟩⟩P.
We have the following derivation.
Notice that Fst(⟨∣c∣⟩)=1 for any c, and Fst((∣T)∣))=T.
[TABLE]
Case 3: L=x::L′, FP(x)=f, where ⊢f:int→τ for some τ.
We have that ⟨⟨L⟩⟩P=Σαf:(∣T∣).Σα1:⟨∣αf∣⟩.Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P.
We now look at Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩C.
We have that αf:T⊢αf:T and ⊢τ:T (notice that ⊢f:int→τ and hence, ⊢int→τ:T and hence, ⊢τ:T).
From ofc_arrow, we have that αf:T⊢αf→τ:T.
From Lemma 7, it follows that αf:T,α1:1⊢αf→τ:T.
From ofs_dyn αf:T,α1:1⊢⟨∣αf→τ∣⟩:sig.
Thus, we have that:
[TABLE]
In addition, by using a reasoning similar to the one in Case 2, we have that:
⊢(∣T∣):sig,
αf:T⊢⟨∣αf∣⟩:sig.
Therefore, we have that:
[TABLE]
Lemma 15
For any L⊆VP, it follows that ⊢⟨⟨L⟩⟩C≤⟨⟨L⟩⟩P:sig.
Proof
We prove the lemma by proving that for any L, ⊢⟨⟨L⟩⟩C≤⟨⟨L⟩⟩P:sig.
We prove this by induction on L.
We have four cases.
Case 1: L=[].
We have that ⟨⟨L⟩⟩C=⟨⟨L⟩⟩P=1.
From eqs_refl, we have that ⊢1≡1:sig and hence, from the subs_refl rule, it follows that ⊢1≤1:sig.
Case 2: L=x::L′ and x∈dom(FP).
We need to prove that ⊢Σαx:(∣S(int)∣).Σα:⟨∣int∣⟩.⟨⟨L′⟩⟩C≤Σαx:(∣T∣).Σα:⟨∣αx∣⟩.⟨⟨L′⟩⟩C:sig.
We first prove that αf:(∣S(int)∣)⊢Σα:⟨∣int∣⟩.⟨⟨L′⟩⟩C≤Σα:⟨∣αx∣⟩.⟨⟨L′⟩⟩C:sig.
To this aim, we prove that
αx:S(int)⊢⟨∣int∣⟩≤⟨∣αx∣⟩:sig.
[TABLE]
From IH, we have that ⊢⟨⟨L′⟩⟩C≤⟨⟨L′⟩⟩P:sig.
From Lemma 7, it follows that αx:S(int),α:1⊢⟨⟨L′⟩⟩C≤⟨⟨L′⟩⟩P:sig.
In addition, from Lemma 14, we have that ⊢⟨⟨L′⟩⟩P:sig.
From Lemma 7, it follows that αx:S(int),α:1⊢⟨⟨L′⟩⟩P:sig.
Since Fst(⟨∣int∣⟩)=Fst(⟨∣αx∣⟩)=1, we have that:
[TABLE]
We next prove that ⊢(∣S(int)∣)≤(∣T∣):sig.
From ofc_int, it follows that ⊢int:T.
From subk_sing_t, it follows that ⊢S(int)≤T:kind.
From subs_stat, it follows that ⊢(∣S(int)∣)≤(∣T∣):sig.
We now prove that αx:T⊢Σα:⟨∣αx∣⟩.⟨⟨L′⟩⟩P:sig.
Indeed, we have that αx:T⊢⟨∣αx∣⟩:sig.
From Lemma 14, ⊢⟨⟨L′⟩⟩P:sig.
From Lemma 7, αx:T,α:1⊢⟨⟨L′⟩⟩P:sig.
From ofs_sigma, it follows that αx:T⊢Σα:⟨∣αx∣⟩.⟨⟨L′⟩⟩P:sig.
Thus, we have that:
[TABLE]
Case 3: L=x::L′ and FP(x)=f, where ⊢f:int→τ for some τ.
We need to prove that
[TABLE]
We first prove that αf:S(int)⊢⟨∣int→τ∣⟩≤⟨∣αf→τ∣⟩:sig.
[TABLE]
We next prove that αf:S(int),α1:1⊢Σα2:⟨∣int→τ∣⟩.⟨⟨L′⟩⟩C≤Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P:sig.
We have that
αf:S(int)⊢⟨∣int→τ∣⟩≤⟨∣αf→τ∣⟩:sig and hence, from Lemma 7, it follows that αf:S(int),α1:1⊢⟨∣int→τ∣⟩≤⟨∣αf→τ∣⟩:sig,
⊢⟨⟨L′⟩⟩C≤⟨⟨L′⟩⟩P:sig (from IH) and hence, from Lemma 7, it follows that αf:S(int),α1:1,α2:1⊢⟨⟨L′⟩⟩C≤⟨⟨L′⟩⟩P:sig,
⊢⟨⟨L′⟩⟩P:sig (from Lemma 14) and hence, from Lemma 7, it follows that αf:S(int),α1:1,α2:1⊢⟨⟨L′⟩⟩P:sig
Since Fst(⟨∣c∣⟩)=1 for any c, we have that:
[TABLE]
We have that:
αf:S(int)⊢⟨∣int∣⟩≤⟨∣αf∣⟩:sig (as in Case 2),
αf:S(int),α1:1⊢Σα2:⟨∣int→τ∣⟩.⟨⟨L′⟩⟩C≤Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P:sig (as proven above),
αf:S(int)⊢αf→τ:T.
From the ofs_dyn rule, αf:S(int)⊢⟨∣αf→τ∣⟩:sig.
From Lemma 7, αf:S(int),α1:1⊢⟨∣αf→τ∣⟩:sig.
From Lemma 14, ⊢⟨⟨L′⟩⟩P:sig and hence, from Lemma 7, αf:S(int),α1:1,α2:1⊢⟨⟨L′⟩⟩P:sig.
Since αf:S(int),α1:1⊢⟨∣αf→τ∣⟩:sig and αf:S(int),α1:1,α2:1⊢⟨⟨L′⟩⟩P:sig, from the ofs_sigma rule, it follows that αf:S(int),α1:1⊢Σα2.⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P:sig.
Since Fst(⟨∣c∣⟩)=1 for any c, we have that:
[TABLE]
We have that
⊢(∣S(int)∣)≤(∣T∣):sig (as in Case 2), and
αf:S(int)⊢Σα1:⟨∣int∣⟩.Σα2:⟨∣int→τ∣⟩.⟨⟨L′⟩⟩C≤Σα1:⟨∣αf∣⟩.Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P:sig (as proven above),
αf:T⊢αf→τ:T.
From the ofs_dyn rule, αf:T⊢⟨∣αf→τ∣⟩:sig.
From Lemma 7, αf:T,α1:1⊢⟨∣αf→τ∣⟩:sig.
From Lemma 14, ⊢⟨⟨L′⟩⟩P:sig and hence, from Lemma 7, αf:T,α1:1,α2:1⊢⟨⟨L′⟩⟩P:sig.
Since αf:T,α1:1⊢⟨∣αf→τ∣⟩:sig and αf:T,α1:1,α2:1⊢⟨⟨L′⟩⟩P:sig, from the ofs_sigma rule, αf:T,α1:1⊢Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P:sig.
Since αf:T⊢αf:T, from the ofs_dyn rule, αf:T⊢⟨∣αf∣⟩:sig.
Since αf:T⊢⟨∣αf∣⟩:sig and αf:T,α1:1⊢Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P:sig, from the ofs_sigma rule, αf:T⊢Σα1:⟨∣αf∣⟩.Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P:sig.
From the subs_sigma rule, we have that
[TABLE]
Lemma 16 (Pitts closure)
For any x, f and a in the policy, it follows that Rx, Rf and Rf∘a are Pitts closed.
Proof
We consider Rx first.
The proof of this case is trivial since any v1 and v2 s.t. ⊢vi:int, we have that ⟨v1,v2⟩∈Rx.
We next consider Rf, where ⊢f:int→τ.
We consider x:int⊢f x.
We have that x is active in f x.
We now consider arbitrary v1 and v2 s.t. ⟨v1,v2⟩ in Rf.
From the definition of Rf, we have that ⟨f v1,f v2⟩∈[[τ]]∅ev.
Since ⊢τ:T, from Lemma 9, we have that ⟨_,_,[[τ]]∅,[[τ]]∅⟩∈[[T]]∅ (notice that ∅∈[[.]]full).
Therefore, [[τ]]∅ is Pitts closed, that is [[τ]]∅=[[τ]]∅st.
Since ⟨f v1,f v2⟩∈[[τ]]∅ev, it follows that ⟨f v1,f v2⟩∈[[τ]]∅stev.
We have proven that:
x is active in f x,
for all ⟨v1,v2⟩∈Rf, ⟨(f x)[x↦v1],(f x)[x↦v2]⟩∈[[τ]]∅stev.
From Lemma 8, for all ⟨w1,w2⟩∈Rfst, we have that ⟨f w1,f w2⟩∈[[τ]]∅stev=[[τ]]∅ev.
From the definition of Rf, we have that ⟨w1,w2⟩∈Rf.
Lemma 17
For any L⊆VP and ρ∈∣L∣P, it follows that
⊢PρL(mP):⟨⟨L⟩⟩C* and ⊢PρR(mP):⟨⟨L⟩⟩C, and*
⊢PρL(mP):⟨⟨L⟩⟩P* and ⊢PρR(mP):⟨⟨L⟩⟩P.*
Proof
The first part of the Lemma 17 is from the definition of ρ∈∣L∣P.
The second part follows from the first part, Lemma 15, and the subsumption rule.
Lemma 18
Suppose that L⊆VP, ρ∈∣L∣P, ρ(αP)=⟨c1,c2,Q⟩, k=Fst(⟨⟨L⟩⟩P).
It follows that:
⊢k:kind,
⊢c1:ρL(k), ⊢c2:ρR(k), and
⟨c1,c2,Q,Q⟩∈[[k]]ρ.
Proof
We prove this lemma by induction on L, using the definition of ρ∈∣L∣P.
Case 1: L=[].
We have that σ=1 and k=1, ρ(αP)=⟨⋆,⋆,⟨⟩⟩.
We can easily check that ⊢1:kind, ⊢⋆:1, and ⟨⋆,⋆,⟨⟩,⟨⟩⟩∈[[1]]ρ.
Case 2: L=x::L′, where x∈dom(FP).
We have that
σ=Σαx:(∣T∣).Σα:⟨∣αx∣⟩.⟨⟨L′⟩⟩P, and
k=Σαx:T.Σα:1.Fst(⟨⟨L′⟩⟩P),
Q=⟨Rx,⟨⟨⟩,Q′⟩⟩,
ρ(αP)=⟨⟨int,⟨⋆,c1′⟩⟩,⟨int,⟨⋆,c2′⟩⟩,⟨Rx,⟨⟨⟩,Q′⟩⟩⟩,
ρ′∈∣L′∣P, where ρ′(αP)=⟨c1′,c2′,Q′⟩.
We need to prove that:
⊢Σαx:T.Σα:1.Fst(⟨⟨L′⟩⟩P):kind,
⊢⟨int,⟨⋆,c1′⟩⟩:ρL(Σαx:T.Σα:1.Fst(⟨⟨L′⟩⟩P)),
⊢⟨int,⟨⋆,c2′⟩⟩:ρL(Σαx:T.Σα:1.Fst(⟨⟨L′⟩⟩P)),
⟨⟨int,⟨⋆,c1′⟩⟩,⟨int,⟨⋆,c2′⟩⟩,⟨Rx,⟨⟨⟩,Q′⟩⟩⟩∈[[Σαx:T.Σα:1.Fst(⟨⟨L′⟩⟩P)]]ρ.
We first prove that ⊢Σαx:T.Σα:1.Fst(⟨⟨L′⟩⟩P):kind.
From IH, we have that ⊢Fst(⟨⟨L′⟩⟩P):kind.
From Lemma 7, α:1⊢Fst(⟨⟨L′⟩⟩P):kind.
From rule ofk_sigma, ⊢Σα:1.Fst(⟨⟨L′⟩⟩P):kind.
From Lemma 7, αx:T⊢Σα:1.Fst(⟨⟨L′⟩⟩P):kind.
From rule ofk_sigma, ⊢Σαx:T.Σα:1.Fst(⟨⟨L′⟩⟩P):kind.
We next prove that ⊢⟨int,⟨⋆,c1′⟩⟩:ρL(Σαx:T.Σα:1.Fst(⟨⟨L′⟩⟩P)) and ⊢⟨int,⟨⋆,c2′⟩⟩:ρL(Σαx:T.Σα:1.Fst(⟨⟨L′⟩⟩P)).
Since their proofs are similar, we only prove here ⊢⟨int,⟨⋆,c1′⟩⟩:ρL(Σαx:T.Σα:1.Fst(⟨⟨L′⟩⟩P)).
Notice that since Σαx:T.Σα:1.Fst(⟨⟨L′⟩⟩P) is a closed kind (as proven above), we have that ρL(Σαx:T.Σα:1.Fst(⟨⟨L′⟩⟩P))=Σαx:T.Σα:1.Fst(⟨⟨L′⟩⟩P).
We have the following derivations.
Notice that
⊢int:T,
if k′ is a closed kind, then k′[β↦c′]=k′ for any β and c′,
⊢c1′:ρL′(Fst(⟨⟨L′⟩⟩P)) (from IH) and hence, ⊢c1′:Fst(⟨⟨L′⟩⟩P) (since from IH, Fst(⟨⟨L′⟩⟩P) is a closed kind).
Thus, ⊢c1′:Fst(⟨⟨L′⟩⟩P)[α↦⋆].
⊢Fst(⟨⟨L′⟩⟩P):kind (from IH) and hence, from Lemma 7, α:1⊢Fst(⟨⟨L′⟩⟩P):kind,
⊢Σα:1.Fst(⟨⟨L′⟩⟩P):kind (from the ofk_sigma rule and α:1⊢Fst(⟨⟨L′⟩⟩P):kind) and hence αx:T⊢Σα:1.Fst(⟨⟨L′⟩⟩P):kind (from Lemma 7).
[TABLE]
[TABLE]
We now prove that ⟨⟨int,⟨⋆,c1′⟩⟩,⟨int,⟨⋆,c2′⟩⟩,⟨Rx,⟨⟨⟩,Q′⟩⟩⟩∈[[Σαx:T.Σα:1.Fst(⟨⟨L′⟩⟩P)]]ρ.
As proven above, we have that ⊢⟨int,⟨⋆,c1′⟩⟩:ρL(Σαx:T.Σα:1.Fst(⟨⟨L′⟩⟩P)) and ⊢⟨int,⟨⋆,c2′⟩⟩:ρR(Σαx:T.Σα:1.Fst(⟨⟨L′⟩⟩P)).
We now need to prove that:
⟨Rx,⟨⟨⟩,Q′⟩⟩∈PreCandsimp(⟨⟨L⟩⟩P),
⟨int,int,Rx,Rx⟩∈[[T]]ρ,
⊢⟨⋆,c1′⟩:ρ1L(Σα:1.Fst(⟨⟨L′⟩⟩P)),
⊢⟨⋆,c2′⟩:ρ1R(Σα:1.Fst(⟨⟨L′⟩⟩P)),
⟨⋆,⋆,⟨⟩,⟨⟩⟩∈[[1]]ρ1
⊢c1′:ρ2L(Fst(⟨⟨L′⟩⟩P)),
⊢c2′:ρ2R(Fst(⟨⟨L′⟩⟩P)),
⟨c1′,c2′,Q′,Q′⟩∈[[Fst(⟨⟨L′⟩⟩P))]]ρ2,
where ρ1=ρ,αx↦⟨int,int,Rx⟩ and ρ2=ρ1,α↦⟨⋆,⋆,⟨⟩⟩.
We have that:
We have that Rx∈PreCandT, ⟨⟩∈PreCand1.
From IH, ⟨c1′,c2′,Q′,Q′⟩∈[[⟨⟨L′⟩⟩P]]ρ′ and hence, Q′∈PreCandsimp(Fst(⟨⟨L′⟩⟩P)) (notice that simp(Fst(⟨⟨L′⟩⟩P))=Fst(⟨⟨L′⟩⟩P) since there is no singleton kind in Fst(⟨⟨L′⟩⟩P)).
From Lemma 16, Rx=Rxst.
Thus, ⟨int,int,Rx,Rx⟩∈[[T]]ρ.
As shown in the first derivation in the proof above, we have that ⊢⟨⋆,c1′⟩:Σα:1.Fst(⟨⟨L′⟩⟩P) and hence, ⊢⟨⋆,c1′⟩:ρ1L(Σα:1.Fst(⟨⟨L′⟩⟩P)) (since Σα:1.Fst(⟨⟨L′⟩⟩P)) is closed)
Similarly, it follows that ⊢⟨⋆,c2′⟩:ρ1R(Σα:1.Fst(⟨⟨L′⟩⟩P)).
Since L′⊆VP and ρ′∈∣L′∣P, from IH, ⊢c1′:ρL′(k′), where ρ′∈∣L′∣P and k′=Fst(⟨⟨L′⟩⟩P)).
Also from IH, ⊢k′.
Thus, ⊢c1′:k′ and hence, ⊢c1′:ρ2L(k′).
Similarly, ⊢c1′:ρ2R(k′).
Since L′⊆VP and ρ′∈∣L′∣P, from IH, ⟨c1′,c2′,Q′,Q′⟩∈[[Fst(⟨⟨L′⟩⟩P)]]ρ′, where ρ′∈∣L′∣P.
Also from IH, ⊢Fst(⟨⟨L′⟩⟩P):kind.
Since ⟨ρ′,ρ2⟩∈[[.]], from Lemma 9, we have that [[Fst(⟨⟨L′⟩⟩P)]]ρ′=[[Fst(⟨⟨L′⟩⟩P)]]ρ2.
Therefore, ⟨c1′,c2′,Q′,Q′⟩∈[[Fst(⟨⟨L′⟩⟩P)]]ρ2.
Case 3: L=x::L′ and FP(x)=f, where ⊢f:int→τ.
We have that ⟨⟨L⟩⟩P=Σαf:(∣T∣).α1:⟨∣αf∣⟩.α2:⟨∣αf→τf∣⟩.⟨⟨L′⟩⟩P, k=Σαf:T.α1:1.α2:1.Fst(⟨⟨L′⟩⟩P), and ρ′(αP)=⟨c1′,c2′,Q′⟩, and
[TABLE]
As in Case 2, we have that ⊢k:kind and ⊢⟨int,⟨⋆,⟨⋆,c1′⟩⟩⟩:k.
We now prove that ⟨c1,c2,Q,Q⟩∈[[Σαf:T.α1:1.α2:1.Fst(⟨⟨L′⟩⟩P)]]ρ.
That is we need to prove that:
⟨Rf,⟨⟨⟩,⟨⟨⟩,Q′⟩⟩⟩∈PreCandsimp(⟨⟨L⟩⟩P),
⟨int,int,Rf,Rf⟩∈[[T]]ρ,
⟨⋆,⋆,⟨⟩,⟨⟩⟩∈[[1]]ρ1, where ρ1=ρ,αf↦⟨int,int,Rf⟩,
⟨⋆,⋆,⟨⟩,⟨⟩⟩∈[[1]]ρ2, where ρ2=ρ1,α1↦⟨⋆,⋆,⟨⟩⟩,
⟨c1′,c2′,Q′,Q′⟩∈[[Fst(⟨⟨L′⟩⟩P)]]ρ3, where ρ3=ρ2,α2↦⟨⋆,⋆,⟨⟩⟩.
The first item can be easily verified (as in Case 2).
From Lemma 16, Rf is Pitts closed and hence, ⟨int,int,Rf,Rf⟩∈[[T]]ρ.
We can easily verify that ⟨⋆,⋆,⟨⟩,⟨⟩⟩∈[[1]]ρ1 and ⟨⋆,⋆,⟨⟩,⟨⟩⟩∈[[1]]ρ2.
We have that L′⊆VP and ρ′∈∣L′∣P (since ρ∈∣L∣P), from IH, we have that ⟨c1′,c2′,Q′,Q′⟩∈[[Fst(⟨⟨L′⟩⟩P)]]ρ′.
Also from IH, we have that ⊢Fst(⟨⟨L′⟩⟩P):kind.
Since ⟨ρ′,ρ3⟩∈[[.]], from Lemma 9, we have that [[Fst(⟨⟨L′⟩⟩P)]]ρ′=[[Fst(⟨⟨L′⟩⟩P)]]ρ3.
Therefore, we have that ⟨c1′,c2′,Q′,Q′⟩∈[[Fst(⟨⟨L′⟩⟩P)]]ρ3.
Lemma 10 (in §0.G)
If ρ1⊨fullP, ρ2⊨fullP, and ΓPP⊢τ:T, then [[τ]]ρ1=[[τ]]ρ2.
Proof
From the definition of ρi∈∣VP∣P,
we have that ρ1(αP)=ρ2(αP)=⟨c1,c2,Q⟩ for some c1, c2, and Q.
From Lemma 18 and the definition of constructor equivalence, we have that:
⊢c1≡c1:ρ1L(Fst(σP)), ⊢c2≡c2:ρ1R(Fst(σP))), and
⟨c1,c2,Q,Q⟩∈[[Fst(σP))]]ρ1.
In other words, ⟨ρ1,ρ2⟩∈[[αP/mP:σP]].
Since ΓPP⊢τ:T, from Lemma 9, we have that ⟨_,_,[[τ]]ρ1,[[τ]]ρ2⟩∈[[T]]ρ1.
From the definition of [[T]]ρ (see Fig. 23), it follows that [[τ]]ρ1=[[τ]]ρ2.
Lemma 11 (in §0.G).
Suppose that ρ⊨fullP.
It follows that ρ∈[[ΓPP]]full.
Proof
We need to prove that ρ⊨full[[αP/mP:⟨⟨VP⟩⟩P]].
We claim that for any L⊆VP and any ρ∈∣L∣P, it follows that ρ⊨full[[αP/mP:⟨⟨L⟩⟩P]].
Then the proof follows directly from the claim.
We now prove the claim.
Suppose that ρ(αP)=⟨c1,c2,Q⟩ and ρ(mP)=⟨V1,V2⟩.
From Lemma 18, we have that:
⊢c1:ρL(k), ⊢c2:ρR(k) where k=Fst(⟨⟨L⟩⟩P), and hence, it follows that ⊢c1≡c1:ρL(k) and ⊢c2≡c2:ρR(k)
⟨c1,c2,Q,Q⟩∈[[k]]ρ.
Therefore, ⟨ρ,ρ⟩∈[[αP/mP:⟨⟨L⟩⟩P]]. Thus, we only need to prove two following items:
ρ(αP)=⟨Fst(V1),Fst(V2),Q⟩,
⟨V1,V2,Q⟩∈[[⟨⟨L⟩⟩P]]ρ.
We prove these two items by induction on L, using the definition of ρ∈∣L∣P.
We have four cases.
Case 1: L=[].
We have that σ=⟨⟨L⟩⟩P=1, ρ(mP)=⟨⋆,⋆⟩ and ρ(αP)=⟨⋆,⋆,⟨⟩⟩.
In other words, V1=V2=⋆ and Q=⟨⟩.
Since ⊢Fst(⋆)≫⋆, from the definition of [[1]]ρ, we have that ⟨V1,V2,Q⟩∈[[σ]]ρ.
Case 2: L=x::L′, x∈dom(FP).
We have that:
[TABLE]
and ⟨v1,v2⟩∈Rx, and ρ′∈∣L′∣P, where ρ′(mP)=⟨V1′,V2′⟩, ρ′(αP)=⟨c1′,c2′,Q′⟩.
We also have that ρ=Σαx:(∣T∣).Σα:⟨∣αx∣⟩.⟨⟨L′⟩⟩P.
Since ρ′(mP)=⟨V1′,V2⟩, ρ′(αP)=⟨c1′,c2′,Q′⟩, and ρ′∈∣L′∣P, from IH, we have that:
c1′=Fst(V1′), c2′=Fst(V2′), and
\langle V_{1}^{\prime},V_{2}^{\prime},Q^{\prime}\rangle\in[\![\langle\!\langle L^{\prime}\rangle\!\rangle_{P}]\!]_{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\rho^{\prime}}}}.
Therefore, we have that Fst(V1)=⟨int,⟨⋆,Fst(V1′)⟩⟩, Fst(V2)=⟨int,⟨⋆,Fst(V2′)⟩⟩.
In other words, ρ(αP)=⟨Fst(V1),Fst(V2),⟨Rx,⟨⟨⟩,Q′⟩⟩⟩.
We now need to prove that ⟨⟨(∣int∣),⟨⟨∣v1∣⟩,V1′⟩⟩,⟨(∣int∣),⟨⟨∣v2∣⟩,V2′⟩⟩,⟨Rx,⟨⟨⟩,Q′⟩⟩⟩∈[[Σαx:(∣T∣).Σα:⟨∣αx∣⟩.⟨⟨L′⟩⟩P]]ρ.
From the definition of [[Σαx:(∣T∣).Σα:⟨∣αx∣⟩.⟨⟨L′⟩⟩P]]ρ, we need to prove that:
⊢IV1:ρL(⟨⟨L⟩⟩P),
⊢IV2:ρR(⟨⟨L⟩⟩P),
⟨(∣int∣),(∣int∣),Rx⟩∈[[(∣T∣)]]ρ,
⟨⟨⟨∣v1∣⟩,V1′⟩,⟨⟨∣v2∣⟩,V2′⟩,⟨⟨⟩,Q′⟩⟩∈[[Σα:⟨∣αx∣⟩.⟨⟨L′⟩⟩P]]ρ1, where ρ1=ρ,αx↦⟨int,int,Rx⟩:
⊢I⟨⟨∣v1∣⟩,V1′⟩:Σα:⟨∣int∣⟩.⟨⟨L′⟩⟩P (since Σα:⟨∣int∣⟩.⟨⟨L′⟩⟩P is a closed signature),
⊢I⟨⟨∣v2∣⟩,V2′⟩:Σα:⟨∣int∣⟩.⟨⟨L′⟩⟩P (since Σα:⟨∣int∣⟩.⟨⟨L′⟩⟩P is a closed signature),
⟨⟨∣v1∣⟩,⟨∣v2∣⟩,⟨⟩⟩∈[[⟨∣αx∣⟩]]ρ1,
⟨V1′,V2′,Q′⟩∈[[⟨⟨L′⟩⟩P]]ρ2, where ρ2=ρ,αx↦⟨int,int,Rx⟩,α↦⟨Fst((∣v1′∣)),Fst((∣v2′∣)),⟨⟩⟩.
These items are proven as below.
From Lemma 17, ⊢PV1:⟨⟨L⟩⟩P and hence ⊢IV1:⟨⟨L⟩⟩P.
From Lemma 14, ⊢⟨⟨L⟩⟩P:sig.
Thus, ⊢IV1:ρL(⟨⟨L⟩⟩P).
Similarly, we have that ⊢IV2:ρR(⟨⟨L⟩⟩P).
From Lemma 16, we have that ⟨int,int,Rx,Rx⟩∈[[T]]ρ and hence, ⟨(∣int∣),(∣int∣),Rx⟩∈[[(∣T∣)]]ρ.
We have that ⊢P⟨∣v1∣⟩:⟨∣int∣⟩.
From Lemma 17, ⊢PV1′:⟨⟨L′⟩⟩C.
Since α∈FV(⟨⟨L′⟩⟩C), from the ofm_pair rule, ⊢P⟨⟨∣v1∣⟩,V1⟩:Σα:⟨∣int∣⟩.⟨⟨L′⟩⟩C.
We have that ⊢⟨∣int∣⟩≤⟨∣int∣⟩:sig, α:1⊢⟨⟨L′⟩⟩C≤⟨⟨L′⟩⟩P:sig, and α:1⊢⟨⟨L′⟩⟩P:sig.
Thus,
[TABLE]
Since ⊢P⟨⟨∣v1∣⟩,V1⟩:Σα:⟨∣int∣⟩.⟨⟨L′⟩⟩C, from ofm_subsume, ⊢P⟨⟨∣v1∣⟩,V1⟩:Σα:⟨∣int∣⟩.⟨⟨L′⟩⟩P.
From the forgetful rule, ⊢I⟨⟨∣v1∣⟩,V1⟩:Σα:⟨∣int∣⟩.⟨⟨L′⟩⟩P.
Similarly, we have that ⊢I⟨⟨∣v2∣⟩,V2′⟩:Σα:⟨∣int∣⟩.⟨⟨L′⟩⟩P,
From the requirement on v1 and v2 in ρ∈∣L∣P, and the definition of [[αx]]ρ,αx↦⟨int,int,Rx⟩, we have that ⟨v1,v2⟩∈[[αx]]ρ,αx↦⟨int,int,Rx⟩ and hence, ⟨⟨∣v1∣⟩,⟨∣v2∣⟩,⟨⟩⟩∈[[⟨∣αx∣⟩]]ρ,αx↦⟨int,int,Rx⟩=[[⟨∣αx∣⟩]]ρ1.
From IH, we have that \langle V_{1}^{\prime},V_{2}^{\prime},Q^{\prime}\rangle\in[\![\langle\!\langle L^{\prime}\rangle\!\rangle_{P}]\!]_{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\rho^{\prime}}}}.
Since ⊢⟨⟨L′⟩⟩P:sig, and ⟨ρ′,ρ2⟩∈[[.]], from Lemma 9, we have that [\![\langle\!\langle L^{\prime}\rangle\!\rangle_{P}]\!]_{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\rho^{\prime}}}}=[\![\langle\!\langle L^{\prime}\rangle\!\rangle_{P}]\!]_{\rho_{2}}.
Therefore, we have that ⟨V1′,V2′,Q′⟩∈[[⟨⟨L′⟩⟩P]]ρ2.
Case 3: L=x::L′, FP(x)=f, where ⊢f:int→τ.
We have that:
[TABLE]
and ⟨v1,v2⟩∈Rf, and ρ′∈∣L′∣P, where ρ′(mP)=⟨V1′,V2′⟩ and ρ′(αP)=⟨c1′,c2′,Q′⟩.
We also have that σ=Σαf:(∣T∣).Σα1:⟨∣αf∣⟩.Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P
The proof that ρ(αP)=⟨Fst(V1),Fst(V2),Q⟩ is similar to the one in Case 2.
We now prove that ⟨V1,V2,Q⟩,∈[[⟨⟨L⟩⟩P]]ρ.
We need to prove that:
⊢IV1:ρL(⟨⟨L⟩⟩P),
⊢IV2:ρR(⟨⟨L⟩⟩P),
⟨⟨∣int∣⟩,⟨∣int∣⟩,Rf⟩∈[[(∣T∣)]]ρ
⟨⟨⟨∣v1∣⟩,⟨⟨∣f∣⟩,V1⟩⟩,⟨⟨∣v2∣⟩,⟨⟨∣f∣⟩,V2′⟩⟩,⟨⟨⟩,⟨⟨⟩,Q′⟩⟩⟩∈[[Σα1:⟨∣αf∣⟩.Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P]]ρ1, where ρ1=ρ,αf↦⟨int,int,Rf⟩
We have that:
From Lemma 17, ⊢PV1:⟨⟨L⟩⟩P and hence ⊢IV1:⟨⟨L⟩⟩P.
From Lemma 14, ⊢⟨⟨L⟩⟩P:sig.
Thus, ⊢IV1:ρL(⟨⟨L⟩⟩P).
Similarly, we have that ⊢IV2:ρR(⟨⟨L⟩⟩P).
From Lemma 16, Rf is Pitts closed.
Thus, ⟨⟨∣int∣⟩,⟨∣int∣⟩,Rf⟩∈[[(∣T∣)]]ρ.
We now prove that
[TABLE]
We need to prove that:
⊢I⟨⟨∣v1∣⟩,⟨⟨∣f∣⟩,V1′⟩⟩:ρ1L(Σα1:⟨∣αf∣⟩.Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P) and hence, ⊢I⟨⟨∣v1∣⟩,⟨⟨∣f∣⟩,V1⟩⟩:Σα1:⟨∣int∣⟩.Σα2:⟨∣int→τ∣⟩.⟨⟨L′⟩⟩P,
⊢I⟨⟨∣v2∣⟩,⟨⟨∣f∣⟩,V2′⟩⟩:ρ1L(Σα1:⟨∣αf∣⟩.Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P) and hence, ⊢I⟨⟨∣v1∣⟩,⟨⟨∣f∣⟩,V1⟩⟩:Σα1:⟨∣int∣⟩.Σα2:⟨∣int→τ∣⟩.⟨⟨L′⟩⟩P,
⟨⟨∣v1∣⟩,⟨∣v2∣⟩,⟨⟩⟩∈[[⟨∣αf∣⟩]]ρ1,
⟨⟨⟨∣f∣⟩,V1′⟩,⟨⟨∣f∣⟩,V2′⟩,⟨⟨⟩,Q′⟩⟩∈[[Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P]]ρ2, where ρ2=ρ1,α1↦⟨⋆,⋆,⟨⟩⟩.
We have that:
By using similar reasoning as in Case 2, ⊢I⟨⟨∣v1∣⟩,⟨⟨∣f∣⟩,V1′⟩⟩:Σα1:⟨∣int∣⟩.Σα2:⟨∣int→τ∣⟩.⟨⟨L′⟩⟩P.
Similarly, ⊢I⟨⟨∣v2∣⟩,⟨⟨∣f∣⟩,V2′⟩⟩:Σα1:⟨∣int∣⟩.Σα2:⟨∣int→τ∣⟩.⟨⟨L′⟩⟩P.
From the definition of ρ∈∣L∣P, ⟨v1,v2⟩∈Rf=[[αf]]ρ,αf↦⟨int,int,Rf⟩.
Thus, ⟨⟨∣v1∣⟩,⟨∣v2∣⟩,⟨⟩⟩∈[[⟨∣αf∣⟩]]ρ,αf↦⟨int,int,Rf⟩=[[⟨∣αf∣⟩]]ρ1.
We now prove that ⟨⟨⟨∣f∣⟩,V1′⟩,⟨⟨∣f∣⟩,V2′⟩,⟨⟨⟩,Q′⟩⟩∈[[Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P]]ρ2.
We need to prove that:
⊢I⟨⟨∣f∣⟩,V1′⟩:ρ2L(Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P) and hence, ⊢I⟨⟨∣f∣⟩,V1′⟩:Σα2:⟨∣int→τ∣⟩.⟨⟨L′⟩⟩P (since Σα2:⟨∣int→τ∣⟩.⟨⟨L′⟩⟩P is a closed signature)
⊢I⟨⟨∣f∣⟩,V2′⟩:ρ2R(Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P) and hence, ⊢I⟨⟨∣f∣⟩,V2′⟩:Σα2:⟨∣int→τ∣⟩.⟨⟨L′⟩⟩P
⟨⟨∣f∣⟩,⟨∣f∣⟩,⟨⟩⟩∈[[⟨∣αf→τ∣⟩]]ρ2
⟨V1′,V2′,Q′⟩∈[[⟨⟨L′⟩⟩P]]ρ3, where ρ3=ρ2,α2↦⟨⋆,⋆,⟨⟩⟩.
We have that:
By using similar reasoning as in Case 2, ⊢I⟨⟨∣f∣⟩,V1′⟩:ρ2L(Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P)
Similarly, ⊢I⟨⟨∣f∣⟩,V2′⟩:ρ2R(Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P)
We consider ⟨w1,w2⟩∈Rf.
From the definition of Rf, ⟨f w1,f w2⟩∈[[τ]]∅ev.
Thus, we have that ⟨f,f⟩∈[[αf→τ]]ρ2.
In other words, ⟨⟨∣f∣⟩,⟨∣f∣⟩,⟨⟩⟩∈[[⟨∣αf→τ∣⟩]]ρ2.
We now prove ⟨V1′,V2′,Q′⟩∈[[⟨⟨L′⟩⟩P]]ρ3.
From IH, ⟨V1′,V2′,Q′⟩∈[[⟨⟨L′⟩⟩P]]ρ′
Since ⟨ρ′,ρ3⟩∈[[.]] and ⊢⟨⟨L′⟩⟩P:sig (Lemma 14), from Lemma 9, we have that [[⟨⟨L′⟩⟩P]]ρ′=[[⟨⟨L′⟩⟩P]]ρ3.
Thus, ⟨V1′,V2′,Q′⟩∈[[⟨⟨L′⟩⟩P]]ρ3.
0.H.2 Wrapper
Lemma 19
If Γ⊢P⟨∣e∣⟩:σ, then σ=⟨∣τ∣⟩ for some τ and Γ⊢e:τ.
Proof
We prove this lemma by induction on the derivation of Γ⊢P⟨∣e∣⟩:σ.
We consider the last rule applied in the derivation.
We have two cases (since other rules cannot be applied).
Case 1: Rule ofm_dyn.
[TABLE]
The proof follows from the rule.
Case 2: Rule ofm_subsume.
[TABLE]
From the rule, we have that Γ⊢P⟨∣e∣⟩:σ′.
From IH, σ′=⟨∣τ′∣⟩ for some τ′ and Γ⊢e:τ′.
Since Γ⊢σ′≤σ:sig, from Lemma 24, Γ⊢σ′≡σ:sig.
From Lemma 23, it follows that σ=⟨∣τ∣⟩ for some τ s.t. Γ⊢τ≡τ′:T.
Thus, Γ⊢e:τ.
Lemma 12 (in §0.G).
If ΓPP⊢e:τ, then ΓCP⊢e.
Proof
First we have that ⊢PλapαP,mP:σP.⟨∣e∣⟩:ΠapαP:σP.(∣τ∣).
[TABLE]
From the weakening lemma (Lemma 7), we have that αP,mP:σPC⊢PλapαP,mP:σP.⟨∣e∣⟩:ΠapαP:σP.(∣τ∣).
In addition, we have that αP,mP:σPC⊢σPC≤σP:sig (Lemma 15 and Lemma 7) and αP,mP:σPC⊢Fst(mP)≫αP.
Therefore, we have that:
[TABLE]
and hence, αP,mP:σPC⊢P(λapαP,mP:σP.⟨∣e∣⟩) mP:(∣τ∣).
Since αP,mP:σPC⊢Fst(mP)≫αP, from mstep_app3,
[TABLE]
And thus,
[TABLE]
From the type preservation theorem ([16, Theorem 2.2]), we have that αP,mP:σPC⊢P⟨∣e∣⟩:(∣τ∣).
From Lemma 19, it follows that αP,mP:σPC⊢Pe.
Lemma 20
It follows that ⊢PVP:σPC.
Proof
We prove the lemma by induction on L.
Lemma 21
It follows that ⊢I(VP:>σP):σP.
Proof
From Lemma 20, we have that ⊢PVP:σPC.
Since ⊢σPC≤σP:sig (by Lemma 15), from the ofm_subsume rule, it follows that ⊢PVP:σP.
From the ofm_forget rule, we have that ⊢IVP:σP.
From the ofm_seal rule, we have that ⊢I(VP:>σP):σP.
Lemma 22
For any V, σ and σ′, if ⊢I(V:>σ):σ′ then ⊢σ≤σ′:sig.
Proof
We prove the lemma by induction on the derivation of ⊢IV:>σ:σ′.
We consider the last rule applied in the derivation.
We have two cases.
Case 1: Rule ofm_seal. From the rule, we have that σ=σ′ and hence, ⊢σ≤σ′:sig.
Case 2: Rule ofm_subsume. From the rule, we have ⊢I(V:>σ):σ′′ and ⊢σ′′≤σ′:sig.
Since ⊢I(V:>σ):σ′′, from IH, ⊢σ≤σ′′:sig.
Since ⊢σ≤σ′′:sig and ⊢σ′′≤σ′:sig, from the subs_trans rule, it follows that ⊢σ≤σ′:sig.
Lemma 23
Suppose that Γ⊢τ:T.
It follows that:
if Γ⊢σ≡⟨∣τ∣⟩:sig, then σ=⟨∣τ′∣⟩ for some τ′ s.t. Γ⊢τ≡τ′:T,
if Γ⊢⟨∣τ∣⟩≡σ:sig, then σ=⟨∣τ′∣⟩ for some τ′ s.t. Γ⊢τ≡τ′:T.
Proof
We prove the lemma by induction on derivation of Γ⊢⟨∣τ∣⟩≡σ:sig and Γ⊢⟨∣τ∣⟩≡σ:sig.
We consider the last rule applied.
We have four cases (other rules cannot be the last rule of the derivation).
Case 1: eqs_refl.
From the rule, we have that σ=⟨∣τ∣⟩.
Since Γ⊢τ:T, from the eqc_reflrule, we have that Γ⊢τ≡τ:T.
Case 2: eqs_symm.
We consider Γ⊢⟨∣τ∣⟩≡σ:sig first.
From the rule, we have that Γ⊢σ≡⟨∣τ∣⟩.
From IH, σ=⟨∣τ′∣⟩ for some τ′ s.t. Γ⊢τ≡τ′:T.
We now consider Γ⊢σ≡⟨∣τ∣⟩:sig.
From the rule, we have that Γ⊢⟨∣τ∣⟩≡σ:sig.
From IH, σ=⟨∣τ′∣⟩ for some τ′ s.t. Γ⊢τ≡τ′:T.
Case 3: eqs_transWe consider Γ⊢⟨∣τ∣⟩≡σ:sig first. From the rule, we have that Γ⊢⟨∣τ∣⟩≡σ′:sig and Γ⊢σ′≡σ:sig.
From IH, it follows that σ′=⟨∣τ′′∣⟩ for some τ′′ s.t. Γ⊢τ≡τ′′:T.
From the static semantics, it follows that Γ⊢τ′′:T.
Thus, from IH, σ=⟨∣τ′∣⟩ for some τ′ s.t. Γ⊢τ′′≡τ′:T.
From the eqc_trans rule, it follows that Γ⊢τ≡τ′:T.
We now consider Γ⊢σ≡⟨∣τ∣⟩:sig. From the rule, we have that Γ⊢σ≡σ′:sig and Γ⊢σ′≡⟨∣τ∣⟩:sig.
From IH, it follows that σ′=⟨∣τ′′∣⟩ for some τ′′ s.t. Γ⊢τ≡τ′′:T.
From the static semantics, it follows that Γ⊢τ′′:T.
Thus, from IH, σ=⟨∣τ′∣⟩ for some τ′ s.t. Γ⊢τ′′≡τ′:T.
From the eqc_trans rule, it follows that Γ⊢τ≡τ′:T.
Case 4: eqs_dyn.
We consider Γ⊢⟨∣τ∣⟩≡σ:sig first.
From the rule, σ=⟨∣τ′∣⟩ for some τ′ and Γ⊢τ≡τ′:T.
We now consider the case Γ⊢σ≡⟨∣τ∣⟩:sig.
From the rule, σ=⟨∣τ′∣⟩ for some τ′ and Γ⊢τ′≡τ:T.
From the eqc_symm rule, it follows that Γ⊢τ≡τ′:T.
Lemma 24
Suppose that Γ⊢⟨∣τ∣⟩≤σ:sig.
It follows that Γ⊢⟨∣τ∣⟩≡σ:sig.
Proof
We prove this lemma by induction on the derivation of Γ⊢⟨∣τ∣⟩≤σ:sig.
We consider the last rule applied.
We have two cases (other rules cannot be the last rule in the derivation).
Case 1: subs_refl.
From the rule, we have that Γ⊢⟨∣τ∣⟩≡σ:sig.
Case 2: subs_trans.
From the rule, we have that Γ⊢⟨∣τ∣⟩≤σ′:sig and Γ⊢σ′≤σ:sig.
Since Γ⊢⟨∣τ∣⟩≤σ′:sig, from IH, we have that Γ⊢⟨∣τ∣⟩≡σ′:sig.
From Lemma 23, σ′=⟨∣τ′∣⟩ for some τ′ s.t. Γ⊢τ≡τ′:T.
Since Γ⊢σ′≤σ:sig, we have that Γ⊢⟨∣τ′∣⟩≤σ:sig.
From IH, we have that Γ⊢⟨∣τ′∣⟩≡σ:sig.
Since σ′=⟨∣τ′∣⟩, it follows that Γ⊢σ′≡σ:sig.
Since Γ⊢⟨∣τ∣⟩≡σ′:sig, and Γ⊢σ′≡σ:sig, we have that Γ⊢⟨∣τ∣⟩≡σ:sig.
Lemma 25
It follows that:
if Γ⊢T≡k:kind then k is T,
if Γ⊢k≡T:kind then k is T,
if Γ⊢1≡k:kind then k is 1,
if Γ⊢k≡1:kind then k is 1.
Proof
We prove this lemma by induction on the derivation of Γ⊢T≡k:kind, Γ⊢k≡T:kind, Γ⊢1≡k:kind, and Γ⊢k≡1:kind.
We have three cases.
Case 1: Rule eqk_refl.
We consider 1 first.
From the rule, we have that k is 1.
The proof for T is similar.
Case 2: Rule eqk_symm.
Case Γ⊢T≡k:kind.
From the rule, Γ⊢k≡T:kind.
From IH, k is T.
Case Γ⊢k≡T:kind.
From the rule, Γ⊢T≡k:kind.
From IH, k is T.
if Γ⊢1≡k:kind.
From the rule, Γ⊢k≡1:kind.
From IH, k is 1.
Case Γ⊢k≡1:kind.
From the rule, Γ⊢1≡k:kind.
From IH, k is 1.
Case 3: Rule eqk_trans.
The proof is similar to the proof of Case 2.
Lemma 26
It follows that:
if Γ⊢1≡σ:sig then σ is 1,
if Γ⊢σ≡1:sig then σ is 1,
if Γ⊢(∣T∣)≡σ:sig then σ is (∣T∣),
if Γ⊢σ≡(∣T∣):sig then σ is (∣T∣).
Proof
We prove the two first items of the lemma by induction on the derivation of Γ⊢1≡σ:sig and Γ⊢σ≡1:sig.
Case 1a: Rule eqs_refl.
From the rule, σ is 1.
Case 2a: Rule eqs_symm.
Case Γ⊢1≡σ:sig. From the rule, Γ⊢σ≡1:sig.
From IH, σ is 1.
Case Γ⊢σ≡1:sig. From the rule, Γ⊢1≡σ:sig.
From IH, σ is 1.
Case 3a: Rule eqs_trans. The proof is similar to the proof of Case 2a.
We prove the last two items of the lemma by induction on the derivation of Γ⊢(∣T∣)≡σ:sig, and Γ⊢σ≡(∣T∣):sig.
Case 1b: Rule eqs_refl.
From the rule, σ is (∣T∣).
Case 2b: Rule eqs_symm.
Case Γ⊢(∣T∣)≡σ:sig.
From the rule, Γ⊢σ≡(∣T∣):sig.
From IH, σ is (∣T∣).
Case Γ⊢σ≡(∣T∣):sig.
From the rule, Γ⊢(∣T∣)≡σ:sig.
From IH, σ is (∣T∣).
Case 3b: Rule eqs_trans.
The proof is similar to the proof of Case 2b.
Case 4b: Rule eqs_stat.
From the rule, σ′=(∣k′∣) for some k′ s.t. Γ⊢T≡k′:kind.
From Lemma 25, k′ is T.
Thus, σ′ is (∣T∣).
Lemma 27
It follows that:
if Γ⊢1≤k:kind then k is 1,
if Γ⊢T≤k:kind then k is T.
Proof
We prove this lemma by induction on the derivation of Γ⊢_≤k:kind.
Here, we only prove the first part of the lemma.
The proof of the second part is similar.
Case 1: Rule subk_refl.
From the rule, Γ⊢1≡k:kind.
From Lemma 25, k is 1.
Case 2: Rule subk_trans.
From the rule, Γ⊢1≤k′:kind and Γ⊢k′≤k:kind.
Since Γ⊢1≤k′:kind, from IH, k′ is 1.
Since Γ⊢k′≤k:kind and k′ is 1, from IH, we have that k is 1.
Lemma 28
It follows that:
if Γ⊢1≤σ:sig then σ is 1,
if Γ⊢(∣T∣)≤σ:sig then σ is (∣T∣).
Proof
We prove the first part of the lemma by induction on the derivation of Γ⊢1≤σ:sig.
Case 1a: Rule subs_refl.
From the rule, Γ⊢1≡σ:sig.
From Lemma 26, σ is 1.
Case 2a: Rule subs_trans.
From the rule, Γ⊢1≤σ′:sig and Γ⊢σ′≤σ:sig.
Since Γ⊢1≤σ′:sig, from IH, σ′ is 1.
Since Γ⊢σ′≤σ:sig and σ′ is 1, from IH, we have that σ is 1.
We now prove the second part of the lemma by induction on the derivation of Γ⊢(∣T∣)≤σ:sig.
Case 1b: Rule subs_refl.
From the rule, Γ⊢(∣T∣)≡σ:sig.
From Lemma 26, σ is (∣T∣).
Case 2b: Rule subs_trans.
From the rule, Γ⊢(∣T∣)≤σ′:sig and Γ⊢σ′≤σ:sig.
Since Γ⊢(∣T∣)≤σ′:sig, from IH, σ′ is (∣T∣).
Since Γ⊢σ′≤σ:sig and σ′ is (∣T∣), from IH, we have that σ is (∣T∣).
Case 3b: Rule subs_stat.
From the rule, σ is k′ s.t. Γ⊢T≤k′:kind.
From Lemma 27, k′=T.
Lemma 29
For any L⊆VP, if Γ⊢⟨⟨L⟩⟩P≤σ:sig for some σ, then Γ⊢⟨⟨L⟩⟩P≡σ:sig.
Proof
We prove the lemma by induction on L.
Case 1: L=[].
We have that ⟨⟨L⟩⟩P=1.
Therefore, we have that ⊢1≤σ:sig.
From Lemma 28, we have that σ is 1.
Thus, Γ⊢1≡σ:sig.
Case 2: L=x::L′ where x∈dom(FP).
We have that ⟨⟨L⟩⟩P=Σαx:(∣T∣).Σα:⟨∣αx∣⟩.⟨⟨L′⟩⟩P.
From the definition of subsignature, σ=Σαx:σ1.Σα:σ2.σ3.
Without loss of generality, we suppose that αx and α are not in dom(Γ) (we can change the constructor variables if necessary).
Therefore, we have that Γ,αx:T ok and Γ,αx:T,α:1 ok.
Since Γ⊢⟨⟨L⟩⟩P≤σ:sig, from the subs_sigma rule, it follows that:
Γ⊢(∣T∣)≤σ1:sig
Γ,αx:T⊢Σα:⟨∣αx∣⟩.⟨⟨L′⟩⟩P≤Σα:σ2.σ3, and hence,
Γ,αx:T⊢⟨∣αx∣⟩≤σ2:sig
Γ,αx:T,α:1⊢⟨⟨L′⟩⟩P≤σ3:sig
We have that:
Γ⊢(∣T∣)≤σ1:sig.
From Lemma 28, σ1 is (∣T∣) and hence, Γ⊢(∣T∣)≡σ1:sig.
Γ,αx:T⊢⟨∣αx∣⟩≤σ2:sig.
From Lemma 24, Γ,αx:T⊢⟨∣αx∣⟩≡σ2:sig.
Γ,αx:T,α:1⊢⟨⟨L′⟩⟩P≤σ3:sig.
From IH, we have that Γ,αx:T,α:1⊢⟨⟨L′⟩⟩P≡σ3:sig.
Therefore, we have the following derivation:
[TABLE]
Case 3: =x::L′ and FP(x)=f, where ⊢f:int→τ.
We have that ⟨⟨L⟩⟩P=Σαf:(∣T∣).Σα1:⟨∣αf∣⟩.Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P.
From the definition of subsignature, σ=Σαf:σ1.Σα1:σ2.Σα2:σ3.⟨⟨L′⟩⟩P.
Without loss of generality, we suppose that αf, α1, and α2 are not in dom(Γ) (we can change the constructor variables if it is necessary).
Therefore, we have that Γ,αf:T ok, Γ,αf:T,α1:1 ok, and Γ,αf:T,α1:1,α2:1 ok.
Since Γ⊢⟨⟨L⟩⟩P≤σ:sig, from the subs_sigma rule, it follows that:
Γ⊢(∣T∣)≤σ1:sig
Γ,αf:T⊢Σα1:⟨∣αf∣⟩.Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P≤Σα1:σ2.Σα2:σ3.σ4, and hence:
Γ,αf:T⊢⟨∣αf∣⟩≤σ2:sig
Γ,αf:T,α1:1⊢Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P≤Σα2:σ3.σ4:sig, and hence,
Γ,αf:T,α1:1⊢⟨∣αf→τ∣⟩≤σ3
Γ,αf:T,α1:1,α2:1⊢⟨⟨L′⟩⟩P≤σ4:sig
As in Case 2, we have that:
Γ,αf:T⊢⟨∣αf∣⟩≡σ2:sig,
Γ,αf:T,α1:1⊢⟨∣αf→τ∣⟩≡σ3,
Γ,αf:T,α1:1,α2:1⊢⟨⟨L′⟩⟩P≡σ4:sig,
Γ⊢(∣T∣)≡σ1:sig,
Therefore, we have the following derivations:
[TABLE]
[TABLE]
Thus, we have that Γ⊢Σαf:(∣T∣).Σα1:⟨∣αf∣⟩.Σα2:⟨∣αf→τ∣⟩.⟨⟨L′⟩⟩P≡Σαf:σ1.Σα1:σ2.Σα2:σ3.σ4.
Lemma 30
Let σ be a signature s.t. Γ⊢σP≡σ:sig.
It follows that Fst(σ)=Fst(σP).
Proof
We claim that for any L⊆VP and σ s.t. ⊢⟨⟨L⟩⟩P≡σ:sig, it follows that Fst(σ)=Fst(⟨⟨L⟩⟩P). The proof then follows directly from the claim.
We prove the claim by induction on L.
Case 1: L=[].
We have that ⟨⟨L⟩⟩P=1.
Since Γ⊢σ≡σP:sig, from Lemma 26, σ=1.
From the definition of Fst(), we have that Fst(σ)=Fst(⟨⟨L⟩⟩P)=1.
Case 2: L=x::L′, where x∈dom(FP).
We have that ⟨⟨L⟩⟩P=Σαx:(∣T∣).Σα:⟨∣αx∣⟩.⟨⟨L′⟩⟩P.
Since ⊢⟨⟨L⟩⟩P≡σ:sig, from the eqs_sigma rule, σ is Σαx:σ1.Σα:σ2.σ3 s.t.
Γ⊢(∣T∣)≡σ1:sig
Γ,αx:T⊢Σα:⟨∣αx∣⟩.⟨⟨L′⟩⟩P≡Σα:σ2.σ3:sig.
Γ,αx:T⊢⟨∣αx∣⟩≡σ2:sig
Γ,αx:T,α:1⊢⟨⟨L′⟩⟩P≡σ3:sig (notice that since αx:T, it follows that Fst(⟨∣τ∣⟩)=1).
We have that:
Γ⊢(∣T∣)≡σ1:sig.
From Lemma 26, σ1=⟨∣T∣⟩.
Thus, Fst(σ1)=T=Fst(⟨∣T∣⟩).
Γ,αx:T⊢⟨∣αx∣⟩≡σ2:sig.
From Lemma 23, σ2=⟨∣τ∣⟩ for some τ s.t. Γ,αx:T⊢αx≡τ:T.
Thus, Fst(σ2)=1=Fst(⟨∣αx∣⟩)
Γ,αx:T,α:1⊢⟨⟨L′⟩⟩P≡σ3:sig.
From IH, we have that Fst(⟨⟨L′⟩⟩P)=Fst(σ3).
Therefore, from the definition of Fst(), we have that Fst(⟨⟨L⟩⟩P)=Fst(σ)
Case 3: L=x::L′, where FP(x)=f.
The proof is similar to the proof of Case 2.
Lemma 31
For any Γ, if Γ⊢σ≡⟨∣τ∣⟩:sig, then σ=⟨∣τ′∣⟩ for some τ′ s.t. Γ⊢τ≡τ′:T.
For any Γ, if Γ⊢⟨∣τ∣⟩≡σ:sig, then σ=⟨∣τ′∣⟩ for some τ′ s.t. Γ⊢τ≡τ′:T.
Proof
We prove the lemma by induction on the derivation of the judgments.
We only have the following cases, since other rules are not applicable.
Case 1: eqs_refl. The proof is trivial.
Case 2: eqs_symm. The proofs of two parts are directly from IH.
Case 3: eqs_trans. The proofs follows from IH and the fact that ≡ of types is transitivity.
Case 4: eqs_dyn. The proofs follows from the rule.
Lemma 32
For any Γ, if Γ⊢σ≤⟨∣τ∣⟩:sig, then σ=⟨∣τ′∣⟩ for some τ′ s.t. Γ⊢τ≡τ′:T.
For any Γ, if Γ⊢⟨∣τ∣⟩≤σ:sig, then σ=⟨∣τ′∣⟩ for some τ′ s.t. Γ⊢τ≡τ′:T.
Proof
We prove both parts of the lemma by induction on the derivation of Γ⊢σ≤⟨∣τ∣⟩:sig and Γ⊢⟨∣τ∣⟩≤σ:sig.
We only have the following cases (other rules are not applicable).
Case 1: subs_refl. The proof follows from Lemma 31.
Case 2: subs_trans.
Part 1: from the rule, Γ⊢σ≤σ′′:sig and Γ⊢σ′′≤⟨∣τ∣⟩:sig.
From IH for Γ⊢σ′′≤⟨∣τ∣⟩:sig, σ′′=⟨∣τ′′∣⟩ for some τ′′ s.t. Γ⊢τ′′≡τ′:T.
Now, we can apply IH on Γ⊢σ≤⟨∣τ′′∣⟩:sig and we have that σ=⟨∣τ′∣⟩ for some τ′ s.t. Γ⊢τ′≡τ′′:T.
Since ≡ for type is transitivity, we have that Γ⊢τ≡τ′:T.
Part 2: the proof is similar.
Lemma 33
If ⊢PwrapP(e):ΠgnαP:σ∗.⟨∣τ∣⟩, where ⊢σ∗≡σP:sig, then αP/mP:σ∗∗⊢I⟨∣e∣⟩:⟨∣τ′∣⟩ for some σ∗∗ and τ′s.t. αP/mP:σ∗∗⊢τ≡τ′ and ⊢σ∗∗≡σP.
Proof
We prove the lemma by induction on the derivation of ⊢PwrapP(e):ΠgnαP:σP.⟨∣τ∣⟩.
Case 1: ofm_lamgn.
From the rule, αP/mP:σ∗⊢I⟨∣e∣⟩:⟨∣τ∣⟩.
Case 2: ofm_subsume.
From the rule, we have ⊢PwrapP(e):ΠgnαP:σ.σ′ s.t. ⊢ΠgnαP:σ.σ′≤ΠgnαP:σ∗.(∣τ∣):sig.
From subs_pigen, we have that ⊢σ∗≤σ:sig and αP:Fst(σ∗)⊢σ′≤⟨∣τ∣⟩:sig.
Since ⊢σ∗≤σ:sig and ⊢σ∗≡σP:sig, we have that ⊢σP≤σ:sig.
From Lemma 29, we have that ⊢σP≡σ:sig.
Since αP:Fst(σ∗)⊢σ′≤⟨∣τ∣⟩:sig, from Lemma 32, we have that σ′=⟨∣τ′∣⟩ for some τ′.
Thus, we have that ⊢PwrapP(e):ΠgnαP:σ.⟨∣τ′∣⟩ s.t. ⊢σ≡σP:sig.
From IH, we close this case.
Lemma 34
If αP/mP:σ⊢I⟨∣e∣⟩:⟨∣τ∣⟩ for some σ s.t. ⊢σ≡σP:sig, then αP/mP:σ⊢P⟨∣e∣⟩:⟨∣τ′∣⟩ for some τ′ s.t. αP/mP:σ⊢τ≡τ′:T.
Proof
We prove the lemma by induction on the derivation of αP/mP:σ⊢I⟨∣e∣⟩:⟨∣τ∣⟩.
We only have the following case:
Case 1: ofm_forget. The proof is directly from the rule.
Case 2: ofm_subsume.
From the rule, we have that αP/mP:σ⊢I⟨∣e∣⟩:σ′ and αP/mP:σ⊢σ′≤⟨∣τ∣⟩:sig.
From Lemma 32, we have that σ′=⟨∣τ′′∣⟩ s.t. αP/mP:σ⊢τ≡τ′′:T.
Thus, we can apply IH on αP/mP:σ⊢I⟨∣e∣⟩:σ′ and close this case.
Lemma 35
If αP/mP:σ⊢P⟨∣e∣⟩:⟨∣τ∣⟩ for some σ s.t. ⊢σ≡σP:sig, then αP/mP:σ⊢e:τ′ for some τ′ s.t. αP/mP:σ⊢τ≡τ′:T.
Proof
We prove the lemma by induction on the derivation of αP/mP:σ⊢P⟨∣e∣⟩:⟨∣τ∣⟩.
We have the following cases.
Case 1: ofm_dyn. The proof is directly from the rule.
Case 2: ofm_subsume. The proof is similar to the proof of Case 2 in Lemma 34.
Lemma 36
If ⊢wrapP(e):ΠgnαP:σP.⟨∣τ∣⟩, then αP/mP:σ⊢e:τ′ for some σ and τ′ s.t. ⊢σ≡σP:sig and αP/mP:σ⊢τ≡τ′:T.
Proof
Since ⊢wrapP(e):ΠgnαP:σP.⟨∣τ∣⟩, from Lemma 33, we have that αP/mP:σ′′⊢I⟨∣e∣⟩:⟨∣τ′′∣⟩ for some σ′′ and τ′′ s.t. ⊢σ′′≡σP:sig and αP/mP:σ′′⊢τ≡τ′′:T.
From Lemma 34 and Lemma 35, we have that αP/mP:σ′⊢e:τ′ for some σ′ and τ′ s.t. ⊢σ′≡σP:sig and αP/mP:σ′⊢τ≡τ′:T.
Theorem 0.G.1 (in §0.G)
If ⊢PwrapP(e):ΠgnαP:σP.⟨∣τ∣⟩, then e is TRNI(P,τ).
Proof
From Lemma 36, we have that αP/mP:σ⊢e:τ′ for some σ and τ′ s.t. ⊢σ≡σP:sig and αP/mP:σ⊢τ≡τ′:T.
From Lemma 30, we have that Fst(σ)=Fst(σP).
In addition, since module variables are not used in the judgments Γ⊢c:k, we have that αP:Fst(σP)⊢τ≡τ′:T.
Thus, we have that αP/mP:σP⊢e:τ.
From Theorem 0.B.2, e is TRNI(P,τ).
Appendix 0.I Computation at different levels
To facilitate the presentation, in this section, we first present the encoding that support computation at different levels only for noninterference.
Then we extend the encoding to support declassification policies.
0.I.1 Language and abstraction theorem
Language.
To have an encoding that support multiple levels, we add the universally quantified types ∀α.τ to the language presented in §2.
In addition, to simplify the encoding, we add the unit type unit.
W.r.t. these new types, we have new values: the unit value ⟨⟩ of unit, and values Λα.e of type ∀α.τ.
Therefore, in addition to the typing rules in §2, we have the following rules.
{mathpar}
{\inferrule*[left={}]{~{}}{\Delta,\Gamma\vdash\langle\rangle:\textbf{unit}}}$${\inferrule*[left={}]{\Delta,\alpha,\Gamma\vdash e:\tau}{\Delta,\Gamma\vdash\Lambda\alpha.e:\forall\alpha.\tau}}$${\inferrule*[left={}]{\Delta,\Gamma\vdash\tau^{\prime}\\
\Delta,\Gamma\vdash\Lambda\alpha.e:\forall\alpha.\tau}{\Delta,\Gamma\vdash e[\tau^{\prime}]:\tau[\tau^{\prime}/\alpha]}}
Similar to the language in §2, the semantics is a call-by-value semantic.
We write λ_:τ.e instead of λx:τ.e when x is not a free variable in e.
Abstraction theorem.
As in §0.F, an environment ρ is a mapping from type variables to tuples of the form ⟨τ1,τ2,R⟩ where R∈Rel(τ1,τ2), and from term variables to tuples of the form ⟨v,v′⟩.
For any ρ s.t. α∈dom(ρ), we write ρ,α↦⟨τ1,τ2,R⟩ to mean the environment ρ′ s.t. dom(ρ′)=dom(ρ)∪{α} and ρ′(β)=⟨τ1,τ2,R⟩ if β=α, and ρ′(β)=ρ(β) otherwise.
For the logical relation, in addition to the rules in Fig. 2, we have other rules described in Fig. 26.
As in §2, we have Lemma 37 about the types of related values and terms are described.
Lemma 37
We have that:
if ⟨v1,v2⟩∈[[τ]]ρ, then ⊢v1:ρL(τ), ⊢v2:ρR(τ) and
if ⟨e1,e2⟩∈[[τ]]ρev, then ⊢e1:ρL(τ) and ⊢e2:ρR(τ).
We write ρ⊨Δ to mean that the domain of ρ is Δ (i.e. dom(ρ)=Δ).
Let ρ∣tv be the restriction of ρ to type variables.
We write ρ⊨Δ,Γ to mean that ρ∣tv⊨Δ and
the set of term variables in dom(ρ) is equal to dom(Γ) (i.e. dom(Γ)={x ∣ x∈dom(ρ)},
for all x∈dom(ρ), ρ(x)∈[[Γ(x)]]ρ.
We define Δ,Γ⊢e1∼e2:τ as in §2 and §0.F.
The following theorem says that the logical equivalence is reflexive.
Theorem 0.I.1 (Abstraction Theorem)
If Δ,Γ⊢e:τ, then Δ,Γ⊢e∼e:τ.
0.I.2 Noninterference for free
0.I.2.1 Overview
We consider noninterference defined for an arbitrary finite security lattice ⟨L,⊑⟩, where L is the set of security levels, and ⊑ is the order between them.
We use lvl as a function from variables to security levels.
We consider programs that read input values from input channels and generate output values to output channels.
Before presenting assumptions on inputs, outputs and programs, we introduce some auxiliary notations.
Let {Wl }l∈L be a family of type constructors indexed by l.
A wrapped value of type τ at level l is a value of type Wl τ.
A wrapped value v can be unwrapped by unwrap k v, where k is an appropriate key and unwrap k v can be implemented as v k.
Below are assumptions on input/output channels and programs.
Assumption 0.I.2
-
Each input/output channel is associated with a security level.
2. 2.
The type of an input value from an input channel is int.
The type of an output value to an output channel is int.151515In this section, the type of inputs/outputs is int. We choose this since we are sticking with [27]. The result presented in this paper can be generalized to accepting confidential inputs of arbitrary types (e.g. Bool, String, etc).
3. 3.
Free variables in programs are considered as inputs from input channels.
4. 4.
Input values on an input channel at level l cannot be directly observed. We model this by using Wl int as their type, not int.
5. 5.
Programs are executed in a context where there are several output channels, each corresponding to a security level.
A program will computes a tuple of wrapped output values, where each element of the tuple is unwrapped by using unwrap and an appropriate key, and the unwrapped value is sent to a channel.
The assumption about execution of programs in the context is illustrated in the following pseudo program, where e is a program satisfying assumptions, o is the computed tuple, Output.Channell is an output channel at l, kl is a key to unwrap value at l, prl projects the output value for the output channel l.
⬇
let* o = e *in
-
IO.Channell1 := unwrap kl1 (πl1o**)*
-
*⋮
-
IO.Channelln := unwrap kln (πlno**)*
Therefore, outputs of considered programs are of the type Wl1 int×⋯×Wln int.
0.I.2.2 Encoding
For every level l in the lattice, we introduce a type variable αl.
To protect data of type τ at level l∈L,
we use a type variable αl and form the type αl→τ.
In other words, Wl int is αl→τ.
Therefore, an input of type int at level l is encoded as a value of type αl→int.
To do computation on values of types αl→τ, programmers have to manage key manually and it is error-prone.
To support handling values of αl→τ, we propose the following interfaces that satisfy monad laws [53, 33] (see proof in §0.I.2.5).
The detailed implementation of them will be described later.
cpl: this interface transfers a wrapped value at l to a continuation and produce an output at l,
wrl: this interface is used to wraps terms.
In addition, we have the interface cvull′ (for l⊏l′) which is used to convert data from a level l to a higher level l′.
Therefore, we have the typing context ΔNI and the term context ΓNI for NI as described in Fig. 27.
Examples illustrating cpl and cvll′ are in Example 22 and Example 23.
161616In these two examples, for illustration purpose, programs only generate single inputs at single levels.
A program generating multiple outputs for multiple levels is illustrated later in Example 25.
Example 22 (Computation at a level)
We consider the lattice ⟨L3,⊑⟩ where L3={L,M,H} and L⊑M⊑H.
Suppose that there are three inputs hi, mi and li and their associated levels are respectively H, M, and L.
By replacing L in Fig. 27 with L3, we have the typing context ΔNI and the term context ΓNI for NI defined on ⟨L3,⊑⟩.
Note that the types of hi, mi and li in ΓNI are respectively αH→int, αM→int, and αL→int.
We now illustrate cp by having a program that has a computation at M: we want to have mi+1.171717Input mi is not of the int type and hence, mi+1 is not well-typed.
We use it just to express the idea of the computation.
This convention is also used in other examples.
In order to use cpM, we first wrap plus_one as below.
[TABLE]
Then we have the following program e1 of the type αM→int encoding the requirement that the function plus_one is applied on y and the result is at M.
[TABLE]
Example 23 (Convert to a higher level)
In this example, we will do the computation hi+mi and the result is at H.
This example illustrates the usage of cvll′ (for l⊏l′).
Let add be a function of the type int→int→int.
From add, we construct wrap_addc of the type int→αH→int,
where c is a variable of the type int.
[TABLE]
The following program e2 of the type αH→int computes the sum of hi and mi and the computed sum is at H.
Note that in order to transfer mi at M to the continuation wrap_addc by using cpH, we need to convert mi from level M to level H by using cvuMH.
[TABLE]
0.I.2.3 Indistinguishability
In this section, we define indistinguishability for an observer ζ∈L. 181818Following [12], we use ζ for observers.
As mentioned in §0.I.2.2, αl is used to protect data at l.
We can think of closed terms related at αl as keys to open wrapped data at l.
Thus, if an observer ζ can observe protected data at l (i.e. l⊑ζ), this observer has the keys.
Otherwise, the observer has no key.
This idea is captured in the following definition, where we use unit as the type of keys, 191919Note that other types can be used. and Fullunit={⟨⟨⟩,⟨⟩⟩}.
202020When another closed type τ is used as the type of keys, we require that all keys are indistinguishable and hence, the substitution for αl is Fullτ when l⊑ζ.
To emphasize this, in Def. 10, we use Fullunit instead of the identity relation on unit, even though for unit, these two relations coincide.
Definition 10
An environment ρ is an environment for noninterference w.r.t. an observer ζ (denoted by ρ⊨ζNI) if ρ⊨ΔNI and for any αl∈ΔNI:
[TABLE]
Note that there is only a unique an environment for NI w.r.t. an observer ζ and hence, hereafter we will use the environment for NI w.r.t. an observer.
We next define indistinguishability for an observer ζ as an instantiation of the logical relation.
Definition 11
Given a type τ s.t. ΔNI⊢τ.
The indistinguishability relations on values and terms of τ for an observer ζ (denoted by resp. INIζ[[τ]] and INIζ[[τ]]ev) are defined as
[TABLE]
where ρ is the environment for NI w.r.t the observer ζ.
Example 24 (Indistinguishability)
We consider the lattice ⟨L3,⊑⟩ described in Example 22.
We will describe the indistinguishability relations of the type αM→int for an observer at L and for an observer at H. Note that αM→int is the type of inputs at level M.
The intuition is that the observer at H can observe data at M and hence, two wrapped values at M are indistinguishable to the observer at H if the wrapped values are the same.
This intuition is captured by the definition of indistinguishability as demonstrated below, where ρ is an environment s.t. ρ⊨HNI.
[TABLE]
Therefore, for any n1 and n2, (λ_:unit.n1,λ_:unit.n2)∈INIH[[αM→int]] iff n1=n2.
While the observer at H can observe data at M, the observer at L cannot.
Therefore, to the observer at L, all wrapped values at M are indistinguishable.
Below is an demonstration showing that indistinguishability for the observer at L is as desired, where ρ⊨LNI.
[TABLE]
Therefore, for any n1 and n2, (λ_:unit.n1,λ_:unit.n2)∈INIH[[αM→int]].
0.I.2.4 Typing implies non-interference
Interface for computation.
The implementations of cpl, cvll′, and wrl are respectively comp, convup, and wrap as below.
The construction of convup and wrap is straightforward.
On a protected input of type unit→β1 and a continuation of type β1→(unit→β2), comp first unfolds the protected input by applying it to the key ⟨⟩ and then applies the continuation on the result.
[TABLE]
We next define a full environment for NI which covers not only type variables but also term variables.
Basically, its restriction to type variables (denoted by ρ∣tv) is the environment for NI w.r.t. an observer ζ.
In addition, it maps inputs to indistinguishable values and interfaces for computation to the specific implementations just defined.
Definition 12
An environment ρ is a full environment for NI w.r.t. an observer ζ (denoted by ρ⊨ζfullNI) if ρ∣tv⊨ζNI and
for all x of the type αl→int (i.e. different from cpl and cvull′),
[TABLE]
for all l, ρ(cpl)=⟨comp,comp⟩,
for all l and l′ s.t. l⊏l′, ρ(cvull′)=⟨convup,convup⟩
for all l, ρ(wrl)=⟨wrap,wrap⟩.
NI for free.
In order to instantiate the abstraction theorem to prove that a program is NI, we need to prove that comp is indistinguishable to itself for any observer and so are convup and wrap.
212121Note that Lemma 38 is not a direct result of the abstraction theorem since the types of implementations (e.g. comp) of defined interfaces are closed types while the types of interfaces (e.g. the type of cpl) are open types.
Lemma 38
For any ζ, it follows that:
[TABLE]
From the definition of ρ⊨ζfullNI and Lemma 38, we have the following corollary.
Corollary 1
For any ρ⊨ζfullNI, ρ⊨ΔNI,ΓNI.
We next prove that if a program is well-typed in ΔNI,ΓNI, then it transforms indistinguishable inputs to indistinguishable outputs.
Theorem 0.I.3
If ΔNI,ΓNI⊢e:τ, then for any ζ∈L and ρ⊨ζfullNI,
[TABLE]
Proof
As proven in Corollary 1, we have that ρ⊨ΔNI,ΓNI.
Since ΔNI,ΓNI⊢e:τ, from Theorem 0.I.1, we have that ⟨ρL(e),ρR(e)⟩∈[[τ]]ρev.
From the definition of indistinguishability, it follows that ⟨ρL(e),ρR(e)⟩∈INIζ[[τ]]ev.
Therefore, we have the following corollary for programs of the type (αl1→int)×⋯×(αln→int).
Corollary 2 (NI for free)
If ΔNI,ΓNI⊢e:(αl1→int)×⋯×(αln→int), then for any ζ∈L and ρ⊨ζfullNI,
[TABLE]
Example 25
By reusing programs in Example 22 and Example 23, we here present of a program that generates output values for levels H, M, and L: the output of the program in this example is of the type (αH→int)×(αM→int)×(αL→int).
To make the paper easier to follow, we recall here e1 and e2 in resp. Example 22 and Example 23.
Programs e1 and e2 compute resp. mi+1 and hi+mi+1.
[TABLE]
Below is the program e that computes output values for all levels.
From Corollary 2, this program is NI.
[TABLE]
0.I.2.5 Monadic encoding
As mentioned earlier, our encoding is a monadic encoding.
We first recall here the monad laws in the popular infix form [53], where wrap and comp are respectively the unit and the bind expressions in monad.
Note that we write e≅e′ when ⟨e,e′⟩∈[[τ]]∅ev which intuitively means that both e and e′ reduce to an equal value.
To simplify the presentation, we do not include types in these laws (e.g. instead of writing wrap[τ] e, we just write wrap e).
[TABLE]
Next we prove that our encoding satisfies monad laws in Lemma 39.
We do not use the infix notation in the lemma. The first, the second and the third parts of the lemma correspond to resp. the left unit, right unit and associativity laws.
Lemma 39
For any closed types τ and τ′:
-
for any e s.t. ⊢e:τ, for any f:τ→unit→τ′,
[TABLE]
2. 2.
for any e s.t. ⊢e:unit→τ,
[TABLE]
3. 3.
for any e s.t. ⊢e:unit→τ, ⊢f:τ→unit→τ′′, ⊢f:τ′′→unit→τ
[TABLE]
0.I.3 Type-based relaxed noninterference for free
0.I.3.1 Declassification policies
Declassification policies considered in this section are similar to the ones in §3, except that since we have multiple levels, for an input at l that can be declassified via f, we need to specify which level it can be declassified to.
Therefore, we define declassification policies as below, where Dec is the set of all closed declassification functions of types int→τf for some closed τf, and ↪ is used to denote partial functions.
Definition 13 (Declassification policies)
A declassification policy P is a tuple ⟨⟨L,⊑⟩,I,lvl,F⟩, where ⟨L,⊑⟩ is a finite lattice of security levels, I is a finite set of inputs, lvl:I→L is a mapping from inputs to security levels, F:I↪(Dec×L) is a partial function from inputs to declassification functions and security levels s.t. if F(x)=⟨f,l⟩ then lvl(x)⊑l.
Example 26 (Policy PMOE)
Consider policy PMOE given by ⟨⟨L3,⊑⟩,I,lvl,F⟩, where
⟨L3,⊑⟩ is the lattice with three levels L, M, and H as described in Example 11,
I={hi,mi,li}: there are three inputs: hi, mi and li,
associated levels of inputs are respectively H, M, and L,
input mi can be declassified via f=λx:int.xmod2 to level L (i.e. F(mi)=(f,L)).
0.I.3.2 Encoding
In this section, we extend the encoding and the indistinguishability relation for NI presented in §0.I.2 to counterparts for declassification policies.
Through this section, we consider a fixed policy P given by ⟨⟨L,⊑⟩,I,lvl,F⟩.
In addition to assumptions in §0.I.2, for declassification policies, we additionally assume that declassifiers are also inputs of programs: that is for each input x that can be declassified via f, we have an input xf which is corresponding for f.
As in NI, we have type variables αl for all levels l∈L, and we also have interfaces cpl, cvull′, and wrl.
The encoding for inputs that cannot be declassified (i.e. inputs that are not in the domain of F) is the same as the encoding for inputs in NI:
the type of an input x at level l is Wl int=αl→int.
We consider an input x at level l that can be declassified via f of the type int→τf to level l′ where l′⊏l.
As for NI, we may use αl→int as the type for this input and require that only observers at l or higher levels have the key to unwrap values at l. However, as explained in Example 24, to an observer at l′, all wrapped values at l are indistinguishable and we do not want this.
Therefore, we introduce a fresh type variable αlf for keys of this input and we require that the observer at l′ also has keys.
Since the observer at l′ has key, if we use αlf→int as the type for the input, as explained in Example 24, only equal values are indistinguishable.
Therefore, we use αlf→αf as the type of the input, where αf is a fresh variable.
We now look at the input xf which corresponds to the declassifier f for x.
Following the idea of the monadic encoding, we can use αf→αl′→τf as the type for xf and we will define an interface cpdecx as below to apply xf to x.
[TABLE]
This interface can be used to apply different functions of type αf→αl′→τf to x.222222Such functions can only handle x via xf or handle x parametrically.
However, we do not need this flexibility.
Therefore, we use (αlf→αf)→αl′→τf as the type for xf.
In addition to xf, in order to support computation on x, we have interface cvx.
The encoding for policy P is described in Fig. 28.
The additional (type and term) variables and conditions are highlighted in blue.
Example 27 (Input declassified correctly)
We consider the PMOE in Example 26.
By using the contexts for PMOE, we can have the program mif mi where the input mi at M is declassified correctly to L via the interface mif.
Example 28 (Computation on input that can be declassified)
Since the type of mi is αMf, in order to do a computation on it, we must convert it as illustrated by the following program, where wrap_plus_one is of the type int→αM→int (the description of this function is in Example 11).
[TABLE]
This program uses cvmi to convert mi to a wrapped value and then transfer it to the continuation wrap_plus_one.
In the context of the policy, this program is of the type αM→int, that is the output of the program is at M.
0.I.3.3 Indistinguishability
As in §0.I.2.3, we first define environments w.r.t. an observer.
The relational interpretation for αl is as in the one for NI: αl is interpreted as pairs of keys to open pairs of protected data.
For αlf which corresponds to x that can be declassified to l′, observers that can observe values at l or l′ can have the key.232323If only observers who can observe values at l have the key, then to an observer at l′, all values at l are indistinguishable (see a similar explanation in Example 24.
Different from the interpretation for αl, the interpretation for αlf directly captures the notion of indistinguishability for values declassified via f.
In other words, the interpretations of αf are different for different observers even though they have keys.
if ζ can observe data at l (i.e. l⊑ζ), then indistinguishable values are equal values,
if ζ can observe declassified data at l′ but not at l (i.e. l′⊑ζ and l⊑ζ), two values v1 and v2 are indistinguishable if they are indistinguishable via f,
otherwise, any two values are indistinguishable.
Let Rf={⟨v1,v2⟩ ∣ ⟨f v1,f v2⟩∈[[τf]]∅}, where ∅ is the empty environment, be the relation s.t. two values are related if via f they behave the same.
Let idint={⟨n,n⟩ ∣ n:int} be the identity relation on int, and Fullint={⟨n,n′⟩ ∣ ⊢n,n′:int} be the full relation on int.
The definition of environments w.r.t. an observer is as below.
Definition 14
An environment ρ is an environment for P w.r.t. an observer ζ (denoted by ρ⊨ζP) if ρ⊨ΔP and
for any αl∈ΔP:
[TABLE]
for any αlf∈ΔP and αlf∈ΔP which corresponds to x s.t. F(x)=(f,l′):
[TABLE]
We next define indistinguishability for P as an instantiation of the logical relation.
The definition is based on the environment of P w.r.t. an observer ζ.
Definition 15
Given a type τ s.t. ΔP⊢τ.
The indistinguishability relations on values and terms of τ for an observer ζ for P (denoted by resp. IPζ[[τ]] and IPζ[[τ]]ev) are defined as
[TABLE]
where ρ is the environment for P w.r.t. the observer ζ.
Example 29 (Indistinguishability for PMOE)
For PMOE presented in Example 26, the type of the input mi that can be declassified to L via f is αMf→αf.
An observer H can observe values at M and hence, two values of mi are indistinguishable when they are equal.
This is indeed captured in Def. 15 and Def. 14:
the observer at H has the key to open wrapped values at M (IPMOEH[[αMf]]=Fullunit), and
two equal integer values are indistinguishable (IPMOEH[[αf]]=idint).
An observer L can only observe values of mi after f.
Therefore, the observer at L has the key to open values (IPMOEL[[αMf]]=Fullunit) and two wrapped values n1 and n2 of mi are indistinguishable if f(n1)=f(n2) as expressed by IPMOEL[[αMf]]=Rf={⟨n1,n2⟩ ∣ f(n1)=f(n2)}.
0.I.3.4 Typing implies security
The implementations for xf and cvx are as below:
[TABLE]
Definition 16
An environment ρ is a full environment for Pw.r.t. an observer ζ (denoted by ρ⊨ζfullP) if ρ∣tv⊨ζP and
for all x of the type αl→int, ρ(x)∈IPζ[[αl→int]],
for all l, ρ(cpl)=⟨comp,comp⟩,
for all l and l′ s.t. l⊏l′, ρ(cvull′)=⟨convup,convup⟩,
for all x of the type αlf→αf, ρ(x)∈IPζ[[αlf→αf]],
for all xf, ρ(xf)=⟨decf,decf⟩,
for all cvx, ρ(cvx)=⟨conv,conv⟩.
In order to instantiate the abstraction theorem to prove security, we need to prove that comp, convup, decf, conv are indistinguishable to themselves for any observer.
Lemma 40
For any ζ, it follows that:
[TABLE]
Lemma 41
For any ζ, for any αlf and αf corresponding to x s.t. lvl(x)=l and F(x)=⟨f,l′⟩:
[TABLE]
We next prove that if a program is well-typed in ΔP, ΓP, then it is type-based relax noninterferent w.r.t. P, that is it transforms indistinguishable inputs to indistinguishable outputs.
Theorem 0.I.4
If ΔP,ΓP⊢e:τ, then for any ζ∈L and ρ⊨ζfullP,
[TABLE]
Proof
Since ρ⊨ζfullP, from the definition of ρ⊨ζfullP, Lemma 40, and Lemma 41, it follows that ρ⊨ζΔP,ΓP.
Since ΔP,ΓP⊢e:τ, from Theorem 0.I.1, we have that ⟨ρL(e),ρR(e)⟩∈[[τ]]ρev.
From the definition of indistinguishability, it follows that ⟨ρL(e),ρR(e)⟩∈IPζ[[τ]]ev.
Corollary 3 (RNI for free)
If ΔP,ΓP⊢e:(αl1→int)×⋯×(αln→int), then for any ζ∈L and ρ⊨ζfullP, it is that ⟨ρL(e),ρR(e)⟩∈IPζ[[(αl1→int)×⋯×(αln→int)]]ev.
0.I.4 Extensions
Similar to the encoding in §4, the encoding in this section can also be extended to support richer policies.
The ideas behind the extensions are similar to the ones in §0.A.
Here we only present two extensions: multiple declassification functions for an input and more inputs involved in a declassification functions (global policies).
The remaining extension is about declassifying via equivalent functions can be obtained by combining the idea in §0.A and §0.I.4.1.
0.I.4.1 More declassification functions
In general an input can be declassified in more than one way.
To show how this can be accommodated, we present an extension for a policy PM1 defined on the lattice ⟨L⋄,⊑⟩, where L⋄={H,M1,M2,L} and L⊑Mi⊑H (for i∈{1,2}).
The input set is I={hi,mi1}, where inputs hi and mi1 are at resp. H and M1.
The policy allows an input to be declassified via multiple functions to different levels.
Specifically, the policy allows that:
input hi can be declassified via f1 to M1 or f2 to M2 for some f1 and f2, where ⊢f1:int→τf1 and ⊢f2:int→τf2,
input mi1 can be declassified via g1 or g2 to L for some g1 and g2, where ⊢g1:int→τg1 and ⊢g2:int→τg2
The policy however, does not allow hi to be declassified to L via g and fi.
For this policy, we have the context described in Fig. 29 where the details of interfaces cpl, cvull′ and wrl are as in Fig. 28 and are omitted.
As in §0.I.3, we have new type variables for inputs hi and mi1 and interfaces hif1, hif2, mi1g1, mi1g2 for declassification functions.
We next define the full environment ρ for PM1 w.r.t. an observer ζ (denoted by ρ⊨ζfullPM1).
For such a ρ, the mapping for term variables is as in Def. 16.
For a type variable αl∈ΔPM1, ρ(αl) is as in Def. 14.
For αHf1,f2, an observer at M1, M2 or H has the key.
[TABLE]
For αf1,f2, the definition is straightforward.
[TABLE]
For αM1g1,g2, all observers have the key (since the input can be declassified to L).
[TABLE]
For αg1,g2, when ζ is L, since this observer can apply g1 and g2 to mi1, two wrapped values are indistinguishable if they cannot be distinguished by both g1 and g2.
In addition, since data at L can flow to M2, for an observer at M2, two wrapped values at M1 are indistinguishable if they are indistinguishable at L.
Therefore, ρ(αg1,g2) is as below:
[TABLE]
where Rg1,g2={(n1,n2) ∣ (g1 n1,g1 n2)∈[[τg1]]∅ev∧(g2 n1,g2 n2)∈[[τg2]]∅ev}.
We define indistinguishability w.r.t. an ζ as an instantiation of the logical relation with an arbitrary ρ⊨ζfullPM1.
The implementations of cp_, cv_, cvull′, hifi, and mi1gi are as in §0.I.3.4.
We also have that these implementations are indistinguishable to themselves for any observer.
Therefore, from the abstraction theorem, we again obtain that for any program e, if ΔPM1,ΓPM1⊢e:τ, then this program maps indistinguishable inputs to indistinguishable outputs.
Proofs are in §0.J.3.
For example, we consider programs eE1=hif1 hi and eE2=⟨mi1g1 mi1⟩.
These programs are well-typed in the context of PM1, and their types are respectively αM→τf1 and αL→τg1 and hence, on indistinguishable inputs, their outputs are indistinguishable at resp. M1 and L.
0.I.4.2 Global policies
We now consider policies where a declassifier can involve more than one input.
For simplicity, in this subsection, we consider a policy PAv defined on the lattice ⟨L⋄,⊑⟩ described in §0.I.4.1.
There are two inputs: mi1 and mi2 at respectively M1 and M2.
The average of these inputs can be declassified to L, i.e. they can be declassified to L via f=λx:int1×int2.(π1x+π2x)/2.242424We can extend the encoding presented in this section to have policies where different subsets of I can be declassified and to have more than one declassifier associated with a set of confidential inputs.
Notice that here we use subscripts for the input type of f to mean that the confidential inputs mi1 and mi2 are corresponding to resp. the first and second elements of an input of f.
To encode the requirement that mi1 and mi2 can be declassified via f, we introduce a new variable y, which is corresponding to the tuple of inputs mi1 and mi2.252525This idea can be generalized to capture the requirement in which there are more than two inputs that can be declassified. When there are n inputs that can be declassified, we just introduce a fresh variable y which is correspond to the n-tuple of inputs.
Individual inputs cannot be declassified, and only y can be declassified via f.
Thus, we have the context described in Fig. 30, where the details of interfaces cpl, cvull′ and wrl are as in Fig. 28 and are omitted
Note that we introduce new type variables αf and αM1,M2f, where αM1,M2f is the type of the key to open y.
Since mi1 cannot be declassified directly, its type is αM1→int.
Similarly, the type of mi2 is αM2→int.
Environment for PAv.
We next define an environment for PAv (denoted by ρ⊨ζPAv).
The definition for ρ⊨ζPAv is similar to Def. 14, except for αM1,M2f and αf.
For αM1,M2f, since y can be declassified to L, all observers have the key.
[TABLE]
Since αf is the type of y which is corresponding to both inputs, its concrete type is int×int.
When ζ=H (i.e. the observer ζ can observe both inputs at M1 and M2), the interpretation of αf is just idint×int.
When ζ=L, since the observer can apply f on y, two tuples of inputs are indistinguishable if the results of f on them are the same.
When ζ=Mi, since declassified data at L can be observed at Mi, two tuples of inputs are indistinguishable if they are indistinguishable at L.
Therefore, we define ρ(αf) as below:
[TABLE]
where Rf∙={⟨⟨v,u⟩,⟨v′,u′⟩⟩ ∣ ⟨f ⟨v,u⟩,f ⟨v′,u′⟩⟩∈[[int]]∅ev}.
Full environment for PAv.
Different from previous sections, in order to define full environments, we need to encode the correspondence between inputs and argument of the declassifier.
We say that an environment ρ of PAv is consistent w.r.t. an ζ if ρ⊨ζPAv and
[TABLE]
This additional condition takes care of the correspondence of inputs and the arguments of the designated declassifier.
We construct decf which is used as the concrete input for yf.
[TABLE]
An environment ρ is full for PAv w.r.t. an ζ (denoted by ρ⊨ζfullPAv) if ρ is consistent w.r.t. ζ, it maps yf to ⟨decf,decf⟩, and the mapping of other term variables is as in Def. 16.
We then define indistinguishability as an instantiation of the logical relation as in Def. 15.
We also have the free theorem saying that if ΔPAv,ΓPAv⊢e:τ, then e maps indistinguishable inputs to indistinguishable outputs.
The proof goes through without changes.
We illustrate this section by considering program yf y where the declassifier is applied correctly.
This program is well-typed in the contexts for PAv and its type is αL→int and hence, this program maps indistinguishable inputs to indistinguishable outputs.
Remark 4
We may use two type variables α1 and α2 for the two inputs (i.e. mi1:α1 and mi2:α2) and use yf:α1×α2→int for the declassifier.
Since we used two type variables separately, we may define the indistinguishability relations for them as the full relation on int.
However, when we define the indistinguishability relations separately, the declassifier f may not be related to itself at α1×α2→int.262626In order to use the abstraction theorem to prove security, we need that the declassifier f is indistinguishable to itself at α1×α2→int.
For example, we have 3 and 4 are indistinguishable at α1, 4 and 5 are indistinguishable at α2 but f ⟨3,5⟩=f ⟨4,6⟩.
To have f related to itself, the indistinguishability relations for α1 and α2 should depend on each other.
For example, suppose that v1 and v1′ are indistinguishable values for mi1.
Then two values v2 and v2′ for mi2 are indistinguishable when f⟨v1,v2⟩=f⟨v1′,v2⟩.
In other words, whether v2 and v2′ are indistinguishable depends on v1 and v1′.
However, we have difficulty to express such dependency between α1 and α2 in the language presented in §0.I.1 and hence, we introduce a new variable y.
Appendix 0.J Proofs for multi-level encodings
0.J.1 Proofs for the encoding for NI
Lemma 37.
Suppose that ρ⊨Δ for some Δ.
It follows that:
if ⟨v1,v2⟩∈[[τ]]ρ, then ⊢v1:ρL(τ), ⊢v2:ρR(τ)and
if ⟨e1,e2⟩∈[[τ]]ρev, then ⊢e1:ρL(τ) and ⊢e2:ρR(τ).
Proof
The second part of the lemma follows directly from rule FR-Term.
We prove the first part of the lemma by induction on structure of τ.
Case 1: int.
We consider ⟨v1,v2⟩∈[[int]]ρ.
From FR-Int, we have that ⊢vi:int.
Since ρL(int)=ρR(int)=int, we have that ⊢v1:ρL(int) and ⊢v2:ρR(int).
Case 2: unit. The proof is similar to the one of Case 1.
We consider ⟨v1,v2⟩∈[[int]]ρ.
From FR-Int, we have that ⊢vi:int.
Since ρL(int)=ρR(int)=int, we have that ⊢v1:ρL(int) and ⊢v2:ρR(int).
Case 3: α.
We consider ⟨v1,v2⟩∈[[α]]ρ.
From the FR-Var rule, ⟨v1,v2⟩∈ρ(α)∈Rel(τ1,τ2).
From the definition of Rel(τ1,τ2), we have that ⊢v1:ρL(α) and ⊢v2:ρR(α).
Case 4: τ1×τ2.
We consider ⟨v1,v2⟩∈[[τ1×τ2]]ρ.
We then have that v1=⟨v11,v12⟩ for some v11 and v12 and v2=⟨v21,v22⟩ for some v21 and v22.
From FR-Pair, it follows that ⟨v11,v21⟩∈[[τ1]]ρ and ⟨v12,v22⟩∈[[τ2]]ρ.
From IH (on τ1 and τ2), we have that ⊢v11:ρL(τ1), ⊢v21:ρR(τ1), ⊢v12:ρL(τ2), and ⊢v22:ρR(τ2).
From FT-Pair, ⊢⟨v11,v12⟩:ρL(τ1)×ρL(τ2) and ⊢⟨v21,v22⟩:ρR(τ1)×ρR(τ2).
Thus, ⊢v1:ρL(τ1)×ρL(τ2) and ⊢v2:ρR(τ1)×ρR(τ2).
In other words, ⊢v1:ρL(τ1×τ2) and ⊢v2:ρR(τ1×τ2).
Case 5: τ1→τ2.
We consider ⟨v1,v2⟩∈[[τ1→τ2]]ρ.
We now look at arbitrary ⟨v1′,v2′⟩∈[[τ1]]ρ.
From FR-Fun, it follows that ⟨v1v1′,v2v2′⟩∈[[τ2]]ρev.
From IH on τ1 and the second part of the lemma on τ2, we have that ⊢v1′:ρL(τ1), ⊢v2′:ρR(τ1), ⊢v1v1′:ρL(τ2), and ⊢v2v2′:ρR(τ2).
From FT-App, we have that ⊢v1:ρL(τ1→τ2) and ⊢v2:ρR(τ1→τ2).
Case 6: ∀α.τ.
We consider an arbitrary R∈Rel(τ1,τ2).
Since ⟨v1,v2⟩∈[[∀α.τ]]ρ,
we have that ⟨v1[τ1],v2[τ2]⟩∈[[τ]]ρ[⟨τ1,τ2,R⟩/α]ev.
From IH, ⊢v1[τ1]:ρL′(τ), where ρ′=ρ[⟨τ1,τ2,R⟩/α].
From the typing rule, ⊢v1:ρL′(∀α.τ).
Since α is bound in τ, we have that ⊢v1:ρL(∀α.τ).
Similarly, ⊢v2:ρR(∀α.τ).
Lemma 38 - Part 1.
For any ζ, it follows that:
[TABLE]
Proof
Let ρ⊨ζNI.
We first prove for cpl:
[TABLE]
From the definition of indistinguishability, we need to prove that:
[TABLE]
where ρ⊨ζNI.
From the definition of the logical relation, we need to prove that for any R∈Rel(τ1,τ1′) and S∈Rel(τ2,τ2′), we have that:
[TABLE]
where ρ′=ρ,β1↦⟨τ1,τ1′,R⟩,β2↦⟨τ2,τ2′,S⟩.
We now need to prove that for all ⟨v,v′⟩∈[[(αl→β1)]]ρ′, for all ⟨f,f′⟩∈[[β1→(αl→β2)]]ρ′, it follows that
[TABLE]
We now have two cases:
l⊑ζ. We have that ρ(αl)=⟨unit,unit,∅⟩ and hence, ⟨f(v ⟨⟩),f′(v′ ⟨⟩)⟩∈[[αl→β2]]ρ′ev holds vacuously.
l⊑ζ. We have that ρ(αl)=⟨unit,unit,Fullunit⟩.
Since ⟨f,f′⟩∈[[β1→(αl→β2)]]ρ′, we just need to prove that ⟨v ⟨⟩,v′ ⟨⟩⟩∈[[β1]]ρ′ev.
And this follows from the fact that ⟨v,v′⟩∈[[αl→β1]]ρ′.
Lemma 38 - Part 2.
For any ζ, it follows that:
[TABLE]
Proof
We need to prove that for any ρ⊨ζNI,
[TABLE]
That is for any closed types τ and τ′, for any R∈Rel(τ,τ′),
[TABLE]
where ρ′=ρ,β↦⟨τ,τ′,R⟩.
From the definition of convup, we need to prove that for any (v,v′)∈[[αl→β]]ρ′, it follows that (v,v′)∈[[αl′→β]]ρ′.
We have the following cases:
l′⊑ζ. Since l⊏l′, we have that l⊏l′⊑ζ.
Since ρ⊨ζNI, we have that ρ(αl)=ρ(αl′)=⟨unit,unit,Fullunit⟩.
Thus, for any ⟨v,v′⟩∈[[αl→β]]ρ′,
We have that ⟨v,v′⟩∈[[αl′→β]]ρ′.
l′⊑ζ.
We have that ρ(αl′)=⟨unit,unit,∅⟩.
Since the interpretation of αl′ is ∅, for any ⟨v,v′⟩∈[[αl→β]]ρ′, we have that ⟨v,v′⟩∈[[αl′→β]]ρ′.
Lemma 38 - Part 3.
For any ζ, it follows that:
[TABLE]
Proof
We need to prove that for any ρ⊨ζNI,
[TABLE]
That is for any τ1, τ2 and R s.t. R∈Rel(τ1,τ2),
[TABLE]
Let ρ′=ρ,β↦⟨τ1,τ2,R⟩, we need to prove that for any (v1,v2)∈R, we have that:
[TABLE]
From the definition of wrap, we need to prove that:
[TABLE]
When l⊑ζ, ρ′(αl)=⟨unit,unit,∅⟩ and hence, the statement hold vacuously.
When l⊑ζ, ρ′(αl)=⟨unit,unit,Fullunit⟩ and hence, we only need to prove that ⟨v1,v2⟩∈R.
This is trivial from the assumption that ⟨v1,v2⟩∈R.
Lemma 39.
For any closed types τ and τ′:
-
for any e s.t. ⊢e:τ, for any f:τ→unit→τ′,
[TABLE]
2. 2.
for any e s.t. ⊢e:unit→τ,
[TABLE]
3. 3.
for any e s.t. ⊢e:unit→τ, ⊢f:τ→unit→τ′′, ⊢f:τ′′→unit→τ
[TABLE]
Proof
We prove (1).
From the definition of wrap, wrap[τ] e\rightarrowtriangle∗λ_:unit.e.
From the definition of comp, we have that:
[TABLE]
Thus, comp[τ][τ′] (wrap[τ] e) f≅f e.
We prove (2).
From the implementation of wrap, wrap[τ]\rightarrowtriangle∗λx:τ.λ_:unit.x.
Let v be the value s.t. e\rightarrowtriangle∗v (note that in our language, all closed terms can be reduced to values).
Let v′ of the type τ s.t. (v ⟨⟩)\rightarrowtriangle∗v′.
Therefore, we have that (e ⟨⟩)\rightarrowtriangle∗v ⟨⟩\rightarrowtriangle∗v′.
From the implementation of comp,
[TABLE]
Thus, (comp[τ][τ′] e wrap[τ]) ⟨⟩\rightarrowtriangle∗v′.
As proven above, (e ⟨⟩)\rightarrowtriangle∗v ⟨⟩\rightarrowtriangle∗v′.
Thus, comp[τ][τ′] e wrap[τ]≅e.
We prove (3).
Let v, v′′′, v′′ and v′ be values s.t.
v is of type unit→τ and e\rightarrowtriangle∗v,
v′′′ is of type τ and v ⟨⟩\rightarrowtriangle∗v′′′,
v′′ is of the type unit→τ′′ s.t. f v′′′\rightarrowtriangle∗v′′
v′ is of the type unit→τ′ s.t. g(v′′ ⟨⟩)\rightarrowtriangle∗v′.
We first look at comp[τ′′][τ′] (comp[τ][τ′′] e f) g.
We have that
[TABLE]
Thus, comp[τ′′][τ′] (comp[τ][τ′′] e f) g\rightarrowtriangle∗g(v′′ ⟨⟩)\rightarrowtriangle∗v′.
We now look at {\mathsf{comp}}[\tau][\tau^{\prime}]\ e\ \big{(}\lambda x:\tau.{\mathsf{comp}}[\tau^{\prime\prime}][\tau^{\prime}]\ (f\ x)\ g\big{)}.
We need to prove that {\mathsf{comp}}[\tau][\tau^{\prime}]\ e\ \big{(}\lambda x:\tau.{\mathsf{comp}}[\tau^{\prime\prime}][\tau^{\prime}]\ (f\ x)\ g\big{)}\rightarrowtriangle^{*}v^{\prime}.
We have that:
[TABLE]
0.J.2 Proofs for the encoding for TRNI
Lemma 40.
For any ζ, it follows that:
[TABLE]
Proof
The proofs for the first three parts are similar to the corresponding ones in Lemma 38.
We now prove the last part.
Let ρ be an environment s.t. ρ⊨ζP.
From Def. 15, we need to prove that
⟨conv,conv⟩∈[[(αlf→αf)→αl→int]]ρ.
That is for any (v,v′)∈[[αlf→αf]]ρ,
[TABLE]
From the definition of conv, we need to prove that:
[TABLE]
We have two cases:
l⊑ζ. We have that ρ(αl)=ρ(αlf)=⟨unit,unit,Fullunit⟩ and ρ(αlf)=⟨int,int,idint⟩.
We need to prove that ⟨v ⟨⟩,v′ ⟨⟩⟩∈[[αf]]ρev.
Since (v,v′)∈[[αfl→αf]]ρ, from ρ(αlf) and ρ(αf) it follows that v ⟨⟩=v′ ⟨⟩.
Therefore, we have that
⟨v,v′⟩∈[[αl→int]]ρ.
l⊑ζ.
We have that ρ(αl)=⟨unit,unit,∅⟩ and hence, ⟨v,v′⟩∈[[αl→int]]ρ vacuously.
Lemma 41.
For any ζ, for any αlf and αf corresponding to x s.t. lvl(x)=l and F(x)=⟨f,l′⟩:
[TABLE]
Proof
Let ρ be an environment s.t. ρ⊨ζP.
From Def. 15, we need to prove that:
[TABLE]
That is for any ⟨v1,v2⟩∈[[αlf→αf]]ρ, ⟨decf v1,decf v2⟩∈[[αl′→τf]]ρev.
From the definition of decf, we need to prove that
[TABLE]
When l′⊑ζ, we have that ρ(αl′)=⟨unit,unit,∅⟩ and hence, the statement holds vacuously.
We now consider the case l′⊑ζ.
We have that ρ(αl′)=⟨unit,unit,Fullunit⟩ and ρ(αlf)=⟨unit,unit,Fullunit⟩.
Therefore we need to prove that
[TABLE]
Let vi′=vi ⟨⟩.
We need to prove that
[TABLE]
Note that since ⟨v1,v2⟩∈[[αlf→αf]]ρ and ρ(αlf)=⟨unit,unit,Fullunit⟩, we have that
[TABLE]
In other words, ⟨v1′,v2′⟩∈[[αf]]ρ.
We have two sub-cases:
l⊑ζ. We have that ρ(αlf)=⟨int,int,Rf⟩.
Since ⟨v1′,v2′⟩∈[[αf]]ρ=Rf, we have that ⟨f v1′,f v2′⟩∈[[τf]]∅ev.
Therefore, ⟨f(v1 ⟨⟩),f(v2 ⟨⟩)⟩∈[[τf]]∅ev and hence, ⟨f(v1 ⟨⟩),f(v2 ⟨⟩)⟩∈[[τf]]ρev (note that τf is a closed type).
l⊑ζ. We have that ρ(αlf)=⟨int,int,idint⟩.
Therefore ⟨v1′,v2′⟩∈idint and hence, v1′=v2′=v.
Since ⊢f v:τf, from Theorem 0.I.1, we have that ⟨f v,f v⟩∈[[τf]]∅ev.
Therefore, ⟨f(v1 ⟨⟩),f(v2 ⟨⟩)⟩∈[[τf]]∅ev and hence, ⟨f(v1 ⟨⟩),f(v2 ⟨⟩)⟩∈[[τf]]ρev (note that τf is a closed type).
0.J.3 Proofs for extensions of the multi-level encoding
0.J.3.1 Proofs for the extension with multiple declassifiers
We prove that the implementations of cp_, cv_, cvu__, hifi, and mi1gi are indistinguishable to themselves for any observer.
Lemma 42
For any ζ, it follows that:
[TABLE]
Proof
The proofs for comp, convup, and wrap are as the corresponding ones in the proof of Lemma 38.
We now prove the first part about conv. The proof for the second part about conv is similar.
Let ρ be an environment s.t. ρ⊨ζfullPM1.
From the definition of indistinguishability, we need to prove that
⟨conv,conv⟩∈[[(αHf1,f2→αf1,f2)→αH→int]]ρ.
That is for any (v,v′)∈[[αHf1,f2→αf1,f2]]ρ,
[TABLE]
From the definition of conv, we need to prove that:
[TABLE]
We have two cases:
H⊑ζ. We have that ρ(αH)=ρ(αHf1,f2)=⟨unit,unit,Fullunit⟩ and ρ(αf1,f2)=⟨int,int,idint⟩.
We need to prove that ⟨v ⟨⟩,v′ ⟨⟩⟩∈[[int]]ρev.
Since (v,v′)∈[[αHf1,f2→αf1,f2]]ρ, from ρ(αH) and ρ(αHf1,f2), it follows that v ⟨⟩=v′ ⟨⟩.
Therefore, we have that ⟨v,v′⟩∈[[αH→int]]ρ.
H⊑ζ.
We have that ρ(αH)=⟨unit,unit,∅⟩ and hence, ⟨v,v′⟩∈[[αl→int]]ρ vacuously.
Lemma 43
For any ζ,
[TABLE]
Proof
We only prove the first part. The proof of the second part is similar.
Let ρ be an environment s.t. ρ⊨ζfullPM1.
From the definition of indistinguishability, we need to prove that:
[TABLE]
That is for any ⟨v1,v2⟩∈[[αHf1,f2→αf1,f2]]ρ, ⟨decf1 v1,decf1 v2⟩∈[[αM1→τf1]]ρev.
From the definition of decf1, we need to prove that
[TABLE]
Let vi′=vi ⟨⟩. We need to prove that:
[TABLE]
When M1⊑ζ, we have that ρ(αM1)=⟨unit,unit,∅⟩ and hence, the statement holds vacuously.
We now consider the case M1⊑ζ.
We have that ρ(αM1)=⟨unit,unit,Fullunit⟩.
Therefore we need to prove that
[TABLE]
Note that since M1⊑ζ, we have that ρ(αf1,f2)=⟨unit,unit,Fullunit⟩.
Since ⟨v1,v2⟩∈[[αHf1,f2→αf1,f2]]ρ, we have that ⟨v1 ⟨⟩,v2 ⟨⟩⟩∈[[αf1,f2]]ρev.
In other words, ⟨v1′,v2′⟩∈[[αf1,f2]]ρ.
We have two sub-cases:
ζ=M1. We have that ρ(αHf1,f2)=⟨int,int,Rf1⟩.
Since ⟨v1′,v2′⟩∈[[αf1,f2]]ρ=Rf1, we have that ⟨f1 v1′,f1 v2′⟩∈[[τf1]]∅ev
and hence, ⟨f1 v1′,f1 v2′⟩∈[[τf1]]ρev (note that τf is a closed type).
Therefore, ⟨f1(v1 ⟨⟩),f1(v2 ⟨⟩)⟩∈[[τf1]]ρev
ζ=H. We have that ρ(αlf1,f2)=⟨int,int,idint⟩.
Therefore ⟨v1′,v2′⟩∈[[αf1,f2]]ρ=idint and hence, v1′=v2′=v.
Since ⊢f1 v:τf, from Theorem 0.I.1, we have that ⟨f1 v,f1 v⟩∈[[τf1]]∅ev and hence, ⟨f1 v,f1 v⟩∈[[τf1]]ρev (note that τf is a closed type).
Thus, ⟨f1(v1 ⟨⟩),f1(v2 ⟨⟩)⟩∈[[τf1]]ρev.
Lemma 44
For any ζ,
[TABLE]
Proof
We only prove the first part. The proof of the second part is similar.
Let ρ be an environment s.t. ρ⊨ζfullPM1.
From the definition of indistinguishability, we need to prove that:
[TABLE]
That is for any ⟨v1,v2⟩∈[[αM1g1,g2→αg1,g2]]ρ, ⟨decg1 v1,decg1 v2⟩∈[[αL→τg1]]ρev.
From the definition of decg1 and the logical relation, we need to prove that
[TABLE]
Let vi′ s.t. vi ⟨⟩\rightarrowtriangle∗vi′.
We need to prove that:
[TABLE]
For all ζ, we have that L⊑ζ and hence, ρ(αL)=⟨unit,unit,Fullunit⟩.
Therefore we need to prove that
[TABLE]
Note that ρ(αM1g1,g2)=⟨unit,unit,Fullunit⟩.
Since ⟨v1,v2⟩∈[[αM1g1,g2→αg1,g2]]ρ, we have that
⟨v1′,v2′⟩∈[[αg1,g2]]ρ.
We have two sub-cases:
M1⊑ζ (i.e. ζ=L or ζ=M2). We have that ρ(αg1,g2)=⟨int,int,Rg1,g2⟩.
Since ⟨v1′,v2′⟩∈[[αg1,g2]]ρ=Rg1,g2, we have that ⟨g1 v1′,g1 v2′⟩∈[[τg1]]∅ev and hence, ⟨g1 v1′,g1 v2′⟩∈[[τg1]]ρev (note that τg1 is a closed type).
M1⊑ζ. We have that ρ(αg1,g2)=⟨int,int,idint⟩.
Therefore ⟨v1′,v2′⟩∈idint and hence, v1′=v2′=v.
Since ⊢g1 v:τf, from Theorem 0.I.1, we have that ⟨g1 v,g1 v⟩∈[[τg1]]∅ev and hence, ⟨g1 v,g1 v⟩∈[[τg1]]ρev (note that τg1 is a closed type).
Theorem 0.J.1
If ΔP,ΓP⊢e:τ, then for any ζ∈L⋄ and ρ⊨ζfullPM1,
[TABLE]
Proof
Since ρ⊨ζfullP, from the definition of ρ⊨ζfullPM1, Lemma 42, Lemma 43, and Lemma 44, it follows that ρ⊨ζΔPM1,ΓPM1.
Since ΔPM1,ΓPM1⊢e:τ, from Theorem 0.I.1, we have that ⟨ρL(e),ρR(e)⟩∈[[τ]]ρev.
From the definition of indistinguishability, it follows that ⟨ρL(e),ρR(e)⟩∈IPM1ζ[[τ]]ev.
0.J.3.2 Proofs for the extension for global policies
The proof of the main result for this extension (in Section 0.I.4.2) is similar to the one in Section 0.I.4.1.
Here, we only prove that decf relates to itself.
Lemma 45
For any ζ,
[TABLE]
Proof
Let ρ be an environment s.t. ρ⊨ζfullPAv.
From the definition of indistinguishability, we need to prove that:
[TABLE]
That is for any ⟨v1,v2⟩∈[[αM1,M2f→αf]]ρ, ⟨decf v1,decf v2⟩∈[[αL→int]]ρev.
From the definition of decf, we need to prove that
[TABLE]
Let vi′ be s.t. vi ⟨⟩\rightarrowtriangle∗vi′.
We need to prove that:
[TABLE]
Since L is the smallest element in the lattice, for all ζ, ρ(αL)=Fullunit.
Thus, we need to prove that f v1′=f v2′.
Note that ρ(αM1,M2f)=⟨unit,unit,Fullunit⟩.
Since ⟨v1,v2⟩∈[[αM1,M2f→αf]]ρ, we have that ⟨v1′,v2′⟩∈[[αf]]ρ.
ζ=H.
We have that ρ(αf)=⟨int×int,int×int,idint×int⟩.
Therefore, we have that v1′=v2′ and hence, f v1′=f v2′.
ζ∈{M1,M2,L}.
We have that ρ(αf)=⟨int×int,int×int,Rf∙⟩, where
[TABLE]
Since ⟨v1′,v2′⟩∈[[αf]]ρ=Rf∙, from the definition of [[int]]∅ev we have that f v1′=f v2′.
