% -*- LaTex -*- \documentclass{article} \usepackage{fullpage} \usepackage{proof} \usepackage{code} \usepackage{macros} \usepackage{amsthm} \usepackage{amssymb} \usepackage{amstext} \usepackage{lang} \usepackage[override]{cmtt} \usepackage{hyperref} \usepackage{rawfootnote} \newtheorem{defn}{Definition} \newtheorem{thm}[defn]{Theorem} \newtheorem{lem}[defn]{Lemma} \newtheorem{con}[defn]{Convention} \newtheorem{prop}[defn]{Proposition} \title{Run-time Principals in Information-flow Type Systems} \author{Stephen Tse \qquad Steve Zdancewic \\\\ Technical Report (MS-CIS-03-39) \\ University of Pennsylvania} \date{} \begin{document} \maketitle % \unmarkedfootnote TODO \rawfootnote{Stephen Tse ({\tt stse@cis.upenn.edu}) and Steve Zdancewic ({\tt stevez@cis.upenn.edu}). This research was supported in part by NSF grant CCR-0311204, \textit{Dynamic Security Policies}. % http://www.cs.berkeley.edu/~daw/oakland04-cfp.html % http://www.ieee.org/organizations/pubs/transactions/information.htm Appears in IEEE Symposium on Security and Privacy, 2004. \\ Last update: \today. } \begin{abstract} Information-flow type systems are a promising approach for enforcing strong end-to-end confidentiality and integrity policies. Such policies, however, are usually specified in term of static information---data is labeled\/ {\em high} or\/ {\em low} security at compile time. In practice, the confidentiality of data may depend on information available only while the system is running. This paper studies language support for\/ {\em run-time principals}, a mechanism for specifying information-flow security policies that depend on which principals interact with the system. We establish the basic property of noninterference for programs written in such language, and use run-time principals for specifying run-time authority in downgrading mechanisms such as declassification. In addition to allowing more expressive security policies, run-time principals enable the integration of language-based security mechanisms with other existing approaches such as Java stack inspection and public key infrastructures. We sketch an implementation of run-time principals via public keys such that principal delegation is verified by certificate chains. \end{abstract} \section{Introduction}\label{sec:intro} Information-flow type systems are a promising approach for enforcing strong end-to-end confidentiality and integrity policies~\cite{SM03}. However, most previous work on these security-typed languages has used simplistic ways of specifying policies: the programmer specifies during program development what data is confidential and what data is public. These information-flow policies constrain which principals have access either directly, or indirectly, to the labeled data. In practice, however, policies are more complex---the principals that own a piece of data may be unknown at compile time or may change over time, and the security policy itself may require such run-time information to downgrade confidential data. This paper addresses these shortcomings and studies \textit{run-time principals} in the context of information-flow policies. Run-time principals are first-class data values representing users, groups, etc. During its execution, a program may inspect a run-time principal to determine policy information not available when the program was compiled. The key problem is designing the language in such a way that the dynamic checks required to implement run-time principals introduce no additional covert channels. Moreover, while adding run-time principals permits new kinds of security policies, the new policies should still interact well with the static type checking. Run-time principals provide a means of integrating the policies expressed by the type system with external notions of principals such as that from public key infrastructure (PKI). This integration allows language-based security mechanisms to interoperate with existing machinery such as the access control policies enforced by a file system or the authentication provided by an OS. This paper makes the following three contributions: \begin{itemize} \item We formalize run-time principals in a simple security-typed language based on the $\lambda$-calculus and show that the type system enforces \textit{noninterference}, a strong information-flow guarantee. This type system is intended to serve as a theoretical foundation for realistic languages such as Jif~\cite{jif} and FlowCaml~\cite{Sim03}. \item We consider the problems of \textit{downgrading} and \textit{delegation} in the presence of run-time principals and propose the concept of \textit{run-time authority} to temper their use. Declassification, and other operations that reveal information owned by a run-time principal, may only be invoked when the principal has granted the system appropriate rights. These capabilities must be verified at runtime, leading to a mechanism reminiscent of (but stronger than) Java's stack inspection~\cite{WF98,WAF00}. \item We investigate the implementation of run-time principals via public key infrastructure. Run-time principals are represented by public keys, run-time authority corresponds to digitally signed capabilities, and the delegation relation between principals can be determined from certificate chains. \end{itemize} As an example of an information-flow policy permitted by run-time principals, consider this program that manipulates data confidential to both a company manager and to less privileged employees: \begin{tightcode} {}1 class C \{ {}2 final principal user = Runtime.getUser(); {}3 void print(String\{user:\} s) \{\ldots\} {}4 void printIfManager(String\{Manager:\} s) \{ {}5 actsFor (user, Manager) \{ {}6 print(s); {}7 \} {}8 \}\} \end{tightcode} This program, written in a Java-like notation, calls the \cd{print} routine to display a string on the terminal. The run-time principal \cd{user}, whose value is determined dynamically (\cd{Runtime.getUser}), represents the user that initiated the program. Note that, in addition to ordinary datatypes such as Java's \cd{String} objects, there is a new basic type, \cd{principal}; values of type \cd{principal} are run-time principals. Lines 3-4 illustrate how information-flow type systems constrain information-flows using labels. The argument to the \cd{print} method is a \cd{String} object \cd{s} that has the static security label \cd{\{user:\}}. In the decentralized label model~\cite{ML98,ML00}, this annotation indicates that \cd{s} is \textit{owned} by the principal \cd{user} and that the policy of \cd{user} is that no other principals can \textit{read} the contents of \cd{s}. This policy annotation indicates that \cd{String}s passed to the \cd{print} method are output on a terminal visible to the principal \cd{user}. More importantly, confidential information such as \cd{Manager}'s password, which \cd{user} is \textit{not} permitted to see, cannot be passed to the \cd{print} method (either directly or indirectly). The type system of the programming language enforces such information-flow policies at compile time without run-time penalty. The \cd{printIfManager} method illustrates how run-time principals can allow for more expressive security policies. This method also takes a \cd{String} as input but, unlike \cd{print}, requires the string to have the label \cd{\{Manager:\}}, meaning that the data is owned and readable only by the principal \cd{Manager}. The body of this method performs a run-time test to determine whether the \cd{user} principal that has initiated the program is in fact acting for the \cd{Manager} principal. If so, then \cd{s} is printed to the terminal, which is secure because the \cd{user} has the privileges of \cd{Manager}. Otherwise \cd{s} is not printed. Without such a run-time test, an information-flow type system would prevent a \cd{String\{Manager:\}} object from being sent to the \cd{print} routine because it expects a \cd{String\{user:\}} object. Run-time principals allows such security policies that depend on the execution environment. Although this example has been explained in terms of Java-like syntax, we carry out our formal analysis of run-time principals in terms of a typed $\lambda$-calculus. This choice allows us to emphasize the new features of run-time principals and to use established proof techniques for noninterference~\cite{HR98, ABHR99, PS02, ZM02}. It should be possible to extend our results to Java-like languages by using the techniques of Banerjee and Naumann~\cite{BN02,BN03}. The rest of the paper is organized as follows. The next section describes our language with run-time principals, including its type system and the noninterference proof. Section~\ref{sec:declassify} considers adding declassification in the context of run-time principals. Section~\ref{sec:pki} suggests how the security policies admitted by our language may be integrated with traditional public key infrastructure and gives an extended example. The last section discusses related work and conclusions. %% \note{What happens if the acts-for hierarchy changes while the program is %% executing? How does that affect the statement of noninterference? %% One observation: if a program has the authority of an (atomic) %% principal p, then the program has two ways of realizing information to %% a second principal q. The first way is to declassify information to %% q. The second is to delegate power to q via the acts-for hierarchy. %% Both are equally difficult, so we don't treat them in the %% noninterference result. Therefore the acts-for hierarchy is statically %% fixed for the duration of the program for the purposes of our %% noninterference proof.} \section{Information-flow type systems} \label{sec:basic} % This section describes \lang{}, an information-flow type system with % support for run-time principals. \subsection{Decentralized label model} The security model considered in this paper is a version of the decentralized label model (DLM) developed by Myers and Liskov~\cite{ML98,ML00}. However, the labels in this paper include integrity constraints in addition to confidentiality constraints, because integrity constraints allow robust declassification (see Section~\ref{sec:declassify}). \para{Principals and labels} Policies in the DLM are described in terms of a set of \textit{principal names}. We use capitalized words like \Alice{}, \Bob{}, \name{Manager}, etc., to distinguish principal names from other syntactic classes of the language. We use meta-variable $X$ to range over such names. To accommodate run-time principals, it is necessary to write policies that refer to principals whose identities are not known statically. Thus, the policy language includes \textit{principal variables}, ranged over by $\alpha$. Principal variables may be instantiated with principal names, as described below. In the example from the introduction, \cd{Manager} is a principal name and the use of \cd{user} in the label is a principal variable. We also need sets of principals, $s$, written as (unordered) comma-separated lists of principals. The empty set (of principals and other syntactic classes), written `$\cdot$', will often be elided. In summary: % \[ \begin{array}{rcl@{\qquad\qquad}rcl} p & \bnf & X \sep \alpha & s & \bnf & \cdot \sep p, s \end{array} \] The confidentiality requirements of the DLM are composed of \textit{reader policy components} of the form \policy{p}{s}, where $p$ is the \textit{owner} of the permissions and $s$ is a set of principals permitted by $p$ to read the data. For example, the component \policy{\Alice{}}{\Bob{},\name{Charles}} says that \Alice{}'s policy is that only \Bob{} and \name{Charles} (and implicitly \Alice{}) may read data with this label. The confidentiality part of the label consists of a set of policy components such that \textit{all} of their restrictions must be obeyed---the principals able to read the data must be in the intersection of the reader permissions. For example, a data labeled with the two reader permissions \policy{\Alice{}}{\Bob{},\name{Charles}} and \policy{\Bob{}}{\name{Charles},\name{Eve}} will be readable only by \name{Charles} and \Bob{}.\footnote{Or, more precisely, principals that can act for \name{Charles} or \name{Bob}; see the discussion of the acts-for hierarchy.} The information-flow type system described below ensures that data with a given confidentiality label will only flow to destinations that are at least that restrictive. This label model is decentralized in the sense that each principal may specify reader sets independently. The integrity part of a label consists of a set of principals that \textit{trust} the data.\footnote{It would be possible to give a version of integrity fully dual to the owners--readers model by using an owners--writers model, but there do not seem to be compelling reasons to do so~\cite{LMZ03}.} For integrity, the information-flow analysis ensures that less trusted data (trusted by fewer principals) is never used where more trusted data is necessary. Collecting the descriptions above, we arrive at the following formal syntax for reader policies $c$, confidentiality policy sets $d$, and labels $l$. The integrity part of a label is separated from the confidentiality part by `\cd{!}': \[ \begin{array}{rcl@{\quad\quad}rcl@{\quad\quad}rcl} c & \bnf & \policy{p}{s} & d & \bnf & \cdot \sep c\mathcd{;}d & l & \bnf & \lbl{d}{s} \end{array} \] \para{Acts-for hierarchy} The decentralized label model also includes \textit{delegation} embodied by a binary \textit{acts-for} relation between principals. This relation is reflexive and transitive, yielding a partial order on principals. The notation $p \delto q$ indicates that principal $q$ acts for principal $p$, or, conversely, that $p$ delegates to $q$. \newcommand{\Albl}{\lbl{\policy{\Alice{}}{}}{\Alice{}}} \newcommand{\Blbl}{\lbl{\policy{\Bob{}}{}}{\Bob{}}} The acts-for hierarchy must be taken into account when determining the restrictions imposed by a label. For example, consider the labels \Albl{} and \Blbl{}. Ignoring the acts-for hierarchy, these labels describe data readable and trusted only by \Alice{} and \Bob{}, respectively. However, if the relation $\Alice{} \delto \Bob{}$ is in the acts-for hierarchy, then data with label \Albl{} will be readable by \Bob{}---because \Bob{} acts for \Alice{}, anything \Alice{} can read \Bob{} can too. Note that \Bob{} does \textit{not} trust the integrity of data with label \Albl{}---\Alice{}'s trust in the data does not imply \Bob{}'s trust. \Alice{} \textit{does} trust data with label \Blbl{}, again because \Bob{} acts for \Alice{}, anything \Bob{} trusts \Alice{} does too. An acts-for hierarchy \D{} is a set of $p \delto q$ constraints. \D{} is \textit{closed} if it contains no principal variables. To make it easier to distinguish closed acts-for hierarchies from potentially open ones, we use the notation \Ahi{} rather than \D{} to mean a closed hierarchy. We write $\D \proves p \delto q$ if principal $q$ acts for principal $p$ according to hierarchy \D{}, or formally, if the reflexive, transitive closure of \D{} contains $p \delto q$. The notation $\Penv \proves \Lsa \delto \Lsb$ extends this delegation relation to sets of principals: The set of principals $s_1$ can act for the set of principals $s_2$ if for each principal $p \in \Lsa$ there exists a principal $q \in \Lsb$ such that $p \delto q$. Furthermore, we assume the existence of the most powerful principal $\top{}$ (called \textit{top}) that acts for all other principals. As a result, for all principals $p$ and all hierarchies \D{}, we have $\D \proves p \delto \top$. \para{Label lattice} The labels of the DLM form a distributive lattice, with join operation given by \[ \lbl{d_1}{s_1} \JOIN \lbl{d_2}{s_2} \defeq \lbl{d_1 \cup d_2}{s_1 \cap s_2} \] A label $l_1$ is less restrictive than a label $l_2$ according to an acts-for hierarchy \D{}, written $\D{} \proves l_1 \sle l_2$, when $l_1$ permits more readers and is at least as trusted. Formally, this relation is defined in according to these two rules (adapted from Myers and Liskov~\cite{ML00} but extended to include integrity sets): \[\Rule{ \forall c_1 \in d_1.\; \exists c_2 \in d_2.\; \LleqD{c_1}{c_2} & \D \proves s_2 \delto s_1 } {\LleqD{\lbl{d_1}{s_1}}{\lbl{d_2}{s_2}}}\] \[\Rule{ \ActsforD{p_1}{p_2} & \forall p_2' \in s_2.\; \exists p_1' \in s_1.\; \ActsforD{p_1'}{p_2'}} {\LleqD{\policy{p_1}{s_1}}{\policy{p_2}{s_2}}}\] We write $\D \proves l_1 \not \sle l_2$ if it is not the case that $\D \proves l_1 \sle l_2$. This negation is well defined because the problem of determining the \sle{} relation is (efficiently) decidable---it reduces to a graph reachability problem over the acts-for hierarchy. The intuition is that the $\sle$ relation describes legal information flows, and the $\not \sle$ relation describes the illegal information flows that should not be permitted in a secure program. According to these rules, the following example label inequalities hold: % \[\begin{array}{rcl} \cdot & \proves & \lbl{\policy{\Alice{}}{\Bob{}}}{} \sle \lbl{\policy{\Alice{}}{}}{} \\ \cdot & \proves & \lbl{\policy{\Alice{}}{}}{} \not \sle \lbl{\policy{\Alice{}}{\Bob{}}}{} \\ \cdot & \proves & \lbl{}{\Alice{},\Bob{}} \sle \lbl{}{\Alice{}} \\ \cdot & \proves & \lbl{}{\Alice{}} \not \sle \lbl{}{\Alice{},\Bob{}} \\ \Alice{} \delto \Bob{} & \proves & \lbl{\policy{\Alice{}}{}}{} \sle \lbl{\policy{\Bob{}}{}}{} \\ \Alice{} \delto \Bob{} & \proves & \lbl{\policy{\Bob{}}{}}{} \not \sle \lbl{\policy{\Alice{}}{}}{} \\ \D & \proves & \Botlbl \sle l \quad \quad \ \ \mbox{(for all \D{} and $l$)} \quad % inter-column space \\ \D & \proves & l \sle \Toplbl \quad \quad \mbox{(for all \D{} and $l$)} \end{array} \] These inequalities show that there is a top-most label \Toplbl{} (owned by $\top$, readable and trusted by no principals) and that the bottom of the label lattice is \Botlbl{} (completely unconstrained readers, trusted by all principals). Data with a less restrictive label may always be treated as having a more restrictive label. % Clearly, \JOIN{} is commutative. It is also easy to verify that for any % two labels $l_1$ and $l_2$ and any acts-for hierarchy \D{} we have $\D % \proves l_1 \sle l_1 \JOIN l_2$. \subsection{\lang{} and run-time principals} This section describes the language \lang{}, a variant of the typed $\lambda$-calculus with information-flow policies drawn from the label lattice described above. In order to focus on run-time principals, \lang{} omits several features which are important for practical programming. First, all programs in \lang{} terminate, thus it precludes termination channels. Second, \lang{} does not have state, so no information channels may arise through the shared memory. Third, the analysis presented here does not consider timing channels. The type system could be extended to remove all of these limitations using known techniques~\cite{VSI96,Aga00,SS01,PS02,ZM02}. Security types, base types, program terms and values of the language are defined according to the grammars in Figure~\ref{fig:grammar}. Like in previous information-flow languages, computation in \lang{} is described by security-types ($t$), which are base types ($u$) annotated with a label ($l$). \begin{figure*} \mbox{ \begin{minipage}[t]{1.9in} \[ \begin{array}{cll} \Tt & ::= \ \Tuly & \mbox{Secure types} \\ \Tu & ::= & \mbox{Base types} \\ & \Tunit & \quad\mbox{unit} \\ & \Tsum\Tt\Tt & \quad\mbox{sum} \\ & \Tfun\Tt\Tt & \quad\mbox{function} \\ & \Tpx & \quad\mbox{principal} \\ & \Tallxp\Tt & \quad\mbox{universal} \end{array} \] \end{minipage} \begin{minipage}[t]{2.5in} \[ \begin{array}{|cll|} e & ::= & \mbox{Terms} \\ & \Vt & \quad\mbox{value} \\ & \Ev & \quad\mbox{variable} \\ & \Einl\Tt\Et & \quad\mbox{left injection}\\ & \Einr\Tt\Et & \quad\mbox{right injection}\\ & \Ecase\Et\Vt\Vt & \quad\mbox{sum case}\\ & \Eapp\Et\Et & \quad\mbox{application}\\ & \Eif\Et\Et\Et\Et & \quad\mbox{if delegation}\\ & \Epapp\Et\Lp & \quad\mbox{instantiation} \end{array} \] \end{minipage} \begin{minipage}[t]{2.2in} \[ \begin{array}{cll} \Vt & ::= & \mbox{Values} \\ & \Eunit & \quad\mbox{unit} \\ & \Einl\Tt\Vt & \quad\mbox{left injection}\\ & \Einr\Tt\Vt & \quad\mbox{right injection}\\ & \Efunx\Tt\Et & \quad\mbox{function}\\ & \Epx & \quad\mbox{principal}\\ & \Eallx\Lp\Et & \quad\mbox{polymorphism} \end{array} \] \end{minipage} } \caption{Syntax of types, terms, and values for \lang{}} \label{fig:grammar} \end{figure*} The unit, sum, and function types are standard~\cite{Pie02}. There is only one value, written \Eunit{}, of type \Tunit{}. Sum values are created by tagging another value $v$ with either the left or right tag: \Einl\Tt\Vt{} and \Einr\Tt\Vt{}, respectively. The \CASE{} expression branches on the tag of a sum value. Function values, of type \Tfun\Tta\Ttb{} are $\lambda$-abstractions of the form \Efun{x}{\Tt}{e}, where $x$ is the formal parameter that is bound within expression $e$, the body of the function. Function application is written by juxtaposition of expressions. By convention, if the label is omitted from a base type, we take it to be the minimal label, \Botlbl{}. For example, the type \Tunitl{\Botlbl} can be written \Tunit{}. We define the type of Booleans with label $l$ to be $\Tulx{\Tbool} \defeq \Tsuml{\Tunit}{\Tunit}$ with values $\TRUE \defeq \Einl{\Tunitl{\Botlbl}}\Eunit$ and $\FALSE \defeq \Einr{\Tunitl{\Botlbl}}\Eunit$. The expression $\IF\;(\Et)\;\Eta\;\Etb$ is encoded as $\Ecase\Et{(\Efun \Eva\Tunit\Eta)}{(\Efun \Evb\Tunit\Etb)}$, for some fresh names $x_1$ and $x_2$. The last two kinds of types, \Tp{\Lp} and \Tallxp\Tt{}, are the new features related to run-time principals. % % It is important to carefully separate principal names, such as % \Alice{}, which are static entities used by the programmer to describe % security policies, from their run-time representations (i.e. the % run-time principals). Thus, while the labels in the types are written % in terms of \Alice{} % The run-time representation of a principal such as \Alice{} may be a public key or some other structured data, but for now we treat these representations as abstract. The only value of type \Tp{\Alice{}} is the constant \Ep\Alice{}. That is, \Tp\Lp{} is a \textit{singleton type}~\cite{aspinall94}; such types have previously been used to represent other kinds of run-time type information~\cite{CWM02}. A program can perform a dynamic test of the acts-for relation between \name{Alice} and \name{Bob} using the expression \Eif{\Ep\Alice}{\Ep\Bob}\Eta\Etb{}. The type \Tallxp\Tt{} is a form of \textit{bounded quantification}~\cite{Pie02} over principals. This type introduces a principal variable, and it describes programs for which the static information about principal $\alpha$ is that the acts-for relation $\alpha \delto \Lp$ holds. For example, the type $t_0 =$ \Tall{\alpha}{\Alice} {\Tfun{\Tul{\Tbool}{\lbl{\policy{\alpha}{}}{}}} {\Tul{\Tbool}{\lbl{\policy{\alpha}{}}{}}}} describes functions whose parameter and return types are Booleans owned by any principal for whom \Alice{} may act. Term-level expressions bind the principal variable $\alpha$ using the syntax \Eallx{\Lp}{e}. If $f$ is such a function of the type $t_0$ given above, and if the acts-for hierarchy establishes that $\Bob \delto \Alice$, we may call $f$ by instantiating $\alpha$ with \Bob{} by \Eapp{\Epapp{f}{\Bob}}{\TRUE}. A bound of $\top$ in a polymorphic type, as in $\Tall{\alpha}{\top}{t}$, expresses a policy parameterized by \textit{any} principal, because all principals satisfy the constraint $p \delto \top$. For convenience, we define the syntactic sugar $\TallS{\alpha}{t} \defeq \Tall{\alpha}{\top}{t}$ and $\EallS{\alpha}{e} \defeq \Eall{\alpha}{\top}{e}$. This kind of polymorphism over principals, in conjunction with the singleton principal types, provides a connection between the static type system and the program's run-time tests of the acts-for hierarchy. Consider the following program $g$, which is similar to the \cd{printIfManager} example in Section~\ref{sec:intro}: \[ \begin{array}{rcl} g & : & \TallS{\alpha} {\Tfun{\Tp{\alpha}} {\Tfun{(\Tfun{\Tul{\Tbool}{\lbl{\policy{\alpha}{}}{}}}{\Tunit})} {\Tfun{\Tul{\Tbool}{\lbl{\policy{\name{M}}{}}{}}} {\Tunit}}}} \\ g & = & \EallS{\alpha} {\Efun{\name{user}}{\Tp{\alpha}} {\Efun{\name{print}}{\Tfun{\Tul{\Tbool}{\lbl{\policy{\alpha}{}}{}}}{\Tunit}} {}}} \\ && \quad{\Efun{\name{s}}{\Tul{\Tbool}{\lbl{\policy{\name{M}}{}}{}}} {\Eif{\Ep{\name{M}}}{\name{user}}{(\Eapp{\name{print}}{s})}{\Eunit}}} \end{array} \] % This function is parameterized by the principal variable $\alpha$. The next parameter is a run-time principal \name{user} that has type \Tp{\alpha}, meaning that the static name associated with the run-time principal \name{user} is $\alpha$. The next two arguments to $g$ are a function called \name{print}, which expects an argument owned by $\alpha$, and a Boolean value $s$, owned by the principal \name{M} (here abbreviating \name{Manager}). The body of $g$ performs a run-time test to determine whether \name{user} acts for \name{M}. If so, the first branch of the conditional is taken, and the \name{print} function is applied to the secret \name{s}. Otherwise, the unit value \Eunit{} is returned. %\input{semantics.tex} \subsection{Evaluation and typing rules} \label{sec:type} \begin{figure*} \mbox{ \begin{minipage}[t]{3.3in} \renewcommand{\arraystretch}{1.2} \[\begin{array}{cl} \Evalx{\Eapp{(\Efunx\Tt\Et)}\Vt}{\Subsx\Et} & \mbox{\vspace{-2em}(E-AppFun)}\\ \Evalx{\Epapp{(\Eallxp\Et)}\Lx}{\Subs\Lv\Lx\Et} & \mbox{\vspace{-2em}(E-PAppAll)} \\ \Evalx{\Ecase{(\Einl\Tt\Vt)}\Vta\Vtb}{\Eapp\Vta\Vt} & \mbox{\vspace{-2em}(E-CaseInl)}\\ \Evalx{\Ecase{(\Einr\Tt\Vt)}\Vta\Vtb}{\Eapp\Vtb\Vt} & \mbox{\vspace{-2em}(E-CaseInr)} \\ \\ \Rule{ \renewcommand{\arraystretch}{1} \begin{array}{l} \Typex\Et{\Tsuml\Tta\Ttb} \\ \Typex\Vta{\Tfunl\Tta\Tt} \\ \Typex\Vtb{\Tfunl\Ttb\Tt} \end{array}} {\Typex{\Ecase\Et\Vta\Vtb}{\join\Tt\Lt}} & \rulelabel{\vspace{-2em}(T-Case)} \\\\ \Rule{ \renewcommand{\arraystretch}{1} \begin{array}{l} \Typex\Eta{\Tpl\Lp} \quad \Typex\Etb{\Tpl\Lq} \\ \Type{\Penv,\Lp\delto\Lq}{\Eenv}{\Etc}{\Tt} \quad \Typex\Etd\Tt \end{array}} {\Typex{\Eif\Eta\Etb\Etc\Etd}{\join\Tt\Lt}} & \rulelabel{\vspace{-2em}(T-IfDel)} \end{array}\] \end{minipage} \begin{minipage}[t]{3in} \renewcommand{\arraystretch}{2.5} \[\begin{array}{cl} \Rule{\Actsfora\Lxa\Lxb} {\Evalx{\Eif{\Ep\Lxa}{\Ep\Lxb}\Etc\Etd}\Etc} & \rulelabel{(E-IfDelYes)}\\ \Rule{\NotActsfora\Lxa\Lxb} {\Evalx{\Eif{\Ep\Lxa}{\Ep\Lxb}\Etc\Etd}\Etd} & \rulelabel{(E-IfDelNo)} \\ \\ \Rule{\LabelD{\Lt}}{\Typex\Epx{\Tpl\Lx}} & \rulelabel{\vspace{-2em}(T-PName)} \\ \Rule{\Type{\Penv,\Lv\delto\Lp}{\Eenv}\Et\Tt & \Lv\not\in\dom\Penv & \LabelD{\Lt}} {\Typex{\Eallx\Lp\Et}{\Tallxpl\Tt}} & \rulelabel{\vspace{-2em}(T-All)} \\ \Rule{\Typex\Et{\Tallxl\Lq\Tt} & \ActsforD\Lp\Lq} {\Typex{\Epapp\Et\Lp}{\join{\Tt\{p/\alpha\}}\Lt}} & \rulelabel{\vspace{-2em}(T-PApp)} \end{array}\] \end{minipage}} \caption{Evaluation and typing rules} \label{fig:rule} \end{figure*} The operational semantics for \lang{} formalizes program evaluation, and the type system keeps track of invariants, which can be statically checked. In this subsection we show that the type system of \lang{} is sound by proving the progress and the preservation theorems. The noninterference theorem of \lang{} uses the soundness property to establish that program security can be checked statically. Figure~\ref{fig:rule} shows the rules for evaluation and typing. \para{Operational semantics} The operational semantics of \lang\ is standard~\cite{Pie02}, except for the addition of the acts-for hierarchy and the if-acts-for test. We use the notation $\Evalx\Et\Etp$ to mean that an acts-for hierarchy \Ahi\ and a program \Et\ make a small step of evaluation to become \Ahi\ and \Etp. The full evaluation of a program is the reflexive and transitive closure of the small-step evaluation. Note that \Ahi\ is used but never changed here; Section~\ref{sec:delegate} considers run-time modification of \Ahi\ via delegation. In Figure~\ref{fig:rule}, E-AppFun says that, if an abstraction \Efunx\Tt\Et\ is applied to a value \Vt, then \Vt\ is substituted for \Ev\ in \Et. Similarly, by E-PAppAll, if a polymorphic term \Eallxp\Et\ is instantiated to a principal \Lx, then \Lx\ is substituted for \Lv\ in \Et. We use the notation \Subsx\Et\ and \Subs\Lv\Lx\Et\ for capture-avoiding substitutions. % Note that we check \Actsfora\Lx\Lp\ statically with % the rule T-PApp of the type system (explained later in this section), % so there is no need to verify this delegation at run-time. E-CaseInl and E-CaseInr are rules for conditional test of tagged values: If the test condition is left-injection \Einl\Tt\Vt, the first branch is applied to \Vt. For example, using the Boolean encoding described earlier, % \[\begin{array}{rcl} && \IF\;(\TRUE)\;\Alice\;\Bob \\ &\defeq& \Ecase{(\Einlx\Eunit)}{(\Efun y\Tunit\Alice)}{(\Efun y\Tunit\Bob)} \\ &\eval& \Eapp{(\Efun y\Tunit\Alice)}\Eunit \\ &\eval& \Alice \end{array}\] E-IfDelYes and E-IfDelNo, unlike the other rules above, use the acts-for hierarchy \Ahi\ to check delegation at run-time. If \Ahi\ proves that principal \Lxa\ delegates to principal \Lxb, the result of an if-acts-for term is the first branch; otherwise, the result is the second branch. \para{Type system} The type system is similar to those previously proposed~\cite{HR98,ZM02,PC00}, except for the addition of rules for run-time principals. The notation \Typex\Et\Tt\ means that a program \Et\ has type \Tt\ under the hierarchy \Penv\ and the term environment \Eenv. To explain how the type system keeps track of information flow, consider the typing rule T-Case for a case term. The test condition has type \Tsuml\Tta\Ttb, the first branch must be a function of type \Tfun\Tta\Tt, and the second branch must be a function of type \Tfun\Ttb\Tt. This typing rule matches the operational semantics of E-CaseInl and E-CaseInr mentioned above. The label of the inputs (the test condition and the branches) will be folded into the label of the output as in \join\Tt\Lt. We define $\join\Tt\Lt=\join{(\Tul\Tu\Ltp)}\Lt=\Tul\Tu{(\join\Ltp\Lt)}$ so that the output always has a label as high as the input's label. For all elimination forms (T-App, T-IfDel and T-PApp), this restriction on the output label is used to rule out implicit information flows~\cite{HR98,ZM02}. By T-PName, only a principal constant \Epx\ has type \Tpl\Lx. This \textit{singleton property} ties the static type information and the run-time identity of principals---if a program expression has type \Tpl{\Lx} it is guaranteed to evaluate to the constant $X$. The extra condition \LabelD\Lt\ checks that the label \Lt\ is well-formed under hierarchy \Penv, meaning that all free principal variables of \Lt\ are contained in \Penv. T-All indicates that a polymorphic term \Eallx\Lp\Et\ is well-typed if the body \Et\ is well-typed under hierarchy \Penv\ extended with the additional delegation \Lv\delto\Lp. The extra condition $\Lv\not\in\dom\Penv$ ensures the well-formedness of the environment---\Lv\ is a fresh variable. T-PApp requires the left term to be a polymorphic term and that the delegation constraint \ActsforD\Lp\Lq\ on the instantiated principal is known statically. T-IfDel is similar to T-All in that it extends \Penv\ with \Lv\delto\Lp, but it does the extension only for the first branch. This matches the operational semantics of E-IfDelYes and E-IfDelNo mentioned above. Extending \Penv\ for the first branch reflects the run-time information that the branch is run only when \Lv\delto\Lp\ holds at run-time. For example, when type-checking the program $g$ from above, the function application $\Eapp{\name{print}}{s}$ will be type-checked in a context where $M \delto \alpha$. Because $M \delto \alpha \proves \lbl{\policy{\name{M}}{}}{} \sle \lbl{\policy{\alpha}{}}{}$ the function application is permitted---inside the first branch of the if-acts-for, a value of type \Tul{\Tbool}{\lbl{\policy{\name{M}}{}}{}} can be treated as though it has type \Tul{\Tbool}{\lbl{\policy{\alpha}{}}{}}. \para{Soundness} The following shows the soundness of the type system with respect to the operational semantics. %% Part 1 of the %% theorem says that if a term \Et\ is closed and has type \Tt\ under %% acts-for hierarchy \Ahi, then either the term is a value or it steps %% to a new term \Etp\ with the same \Ahi. Part 2 says if \Et\ is closed, %% has type \Tt\ and steps to \Etp, then \Etp\ also has type \Tt. The %% result means that if we type-check a program, then its type invariant %% is preserved along its computation and its computation always %% terminates at a value. \begin{thm}[Soundness]\label{thm-sound} (1) Progress: If $\Typea\Et\Tt$, then $\Et=\Vt$ or $\Evalx\Et\Etp$. (2) Preservation: If $\Typea\Et\Tt$ and $\Evalx\Et\Etp$, then $\Typea\Etp\Tt$. \end{thm} The proof for this theorem is standard for languages with subtyping~\cite{Pie02}. Appendix contains the complete proof, which uses the following substitution lemma. The lemma says that if an open term \Et\ has type \Tt, then the substituted term $\Epsx\Et$ has the substituted type \Psx\Tt---this result is also needed to prove noninterference later (Theorem~\ref{thm:nonni} and Lemma~\ref{lem:subs-logical}). Substitution also respects subtyping for types, principals, labels and policies~\cite{TZ03b}. % The notation \Pmodx\ denotes a substitution \Ps\ that assigns each free principal variable \Lv\ in hierarchy \Penv\ to a principal name \Lx. Similarly, $\Emodz{\Psx\Eenv}$ denotes a term substitution \Es\ that assigns each free term variable \Ev\ in environment \Eenv\ to a value such that the assignment respects the typing $\Ev:\Tt$ in \Eenv. % Part 1 of the substitution lemma below says that if an open term \Et\ % has type \Tt, then the substituted term $\Epsx\Et$ has the substituted % type \Psx\Tt. Part 2 and Part 3 say that substitution respects % subtyping for principals and for types in a similar % way.\footnote{Substitution also respects subtyping for labels and % policies, but for brevity we do not state the result here.} \begin{lem}[Substitution for typing]\label{lem:subs-sub}\ \\ If $\Typex\Et\Tt$, $\Pmodx$, $\Ahi=\Psx\Penv$ and $\Emodz{\Psx\Eenv}$, then $\Typea{\Epsx\Et}{\Psx\Tt}$. \end{lem} \subsection{Noninterference} \label{sec:noninterference} \begin{figure*} \renewcommand{\arraystretch}{2.5} \[\begin{array}{clcl} \Rule{ \Ahi\proves\Eenv \quad\Emodz\Eenv \quad\Emodzp\Eenv \\ \forall(\Ev:\Tt\in\Eenv).\; \Relv{\Esx\Ev}{\Esxp\Ev}\Tt} \Relgx & \rulelabel{(R-Sub)} & \Rule{\Ahi\proves\Lt\not\sle\Rell} {\Relvx\Tuly} & \rulelabel{(R-Label)} \\ \Rule{ \renewcommand{\arraystretch}{1} \begin{array}{l} \Evalmx\Et\Vt \quad\Evalmx\Etp\Vtp \\ \Typea\Et\Tt \quad\Typea\Etp\Tt \quad\Relvx\Tt \end{array}} {\Relex\Tt} & \rulelabel{(R-Term)} & \raisebox{1.5ex}{\mbox{\Relv\Eunit\Eunit\Tunitlx}} & \mbox{(R-Unit)} \\ \Rule{ \forall(\Relvb\Tta).\; \Rele{(\Eapp\Vt\Vtb)}{(\Eapp\Vtp\Vtbp)}{\join\Ttb\Lt}\Rell} {\Relvx{\Tfunl\Tta\Ttb}} & \rulelabel{(R-Fun)} & \raisebox{1.5ex}{\mbox{\Relv\Epx\Epx{\Tpl\Lx} }} & \mbox{(R-PName)} \\ \Rule{\forall(\Actsfora\Lx\Lp).\; \Rele{(\Epapp\Vt\Lx)}{(\Epapp\Vtp\Lx)}{\join\Tt\Lt}\Rell} {\Relvx{\Tallxpl\Tt}} & \rulelabel{(R-All)} & \Rule{\Relvx\Tta} {\Relv{\Einlx\Vt}{\Einlx\Vtp}{\Tsuml\Tta\Ttb}} & \rulelabel{(R-Inl)} \end{array}\] \caption{Logical relations for types with labels} \label{fig:logical} \end{figure*} This section proves a noninterference theorem~\cite{GM82}, which is the first main theoretical result of this paper. The intuition is that in secure programs, high-security inputs do not interfere with low-security outputs. Formally, the noninterference theorem states that if a Boolean program \Et\ of low security \Lt\ is closed and well-typed but contains a free variable \Ev\ of high security \Ltp, and if values \Vt\ and \Vtp\ have the same type and security as \Ev, then substituting either \Vt\ or \Vtp\ for \Ev\ in \Et\ will evaluate to the same Boolean value \Vtz. We use Boolean so that the equivalence of the final values can be observed syntactically. This result means that a low-security observer cannot use program \Et\ to learn information about input \Ev. \begin{thm}[Noninterference]\label{thm:nonni} If $\Type\Ahi{\Ev:\Tul\Tu\Ltp}\Et\Tboollx$, $\Ahi\proves\Ltp\not\sle\Lt$, $\Typea\Vt{\Tul\Tu\Ltp}$ and $\Typea\Vtp{\Tul\Tu\Ltp}$ then \[ \Evalmx{\Subs\Ev\Vt\Et}\Vtz \quad\mbox{iff}\quad \Evalmx{\Subs\Ev\Vtp\Et}\Vtz \] \end{thm} The proof requires a notion of equivalence with respect to observers of different security labels. To reason about equivalence of higher-order functions and polymorphism, we use the standard technique of logical relations~\cite{Mit96}. However, we parameterize the relations with an upper-bound \Rell\ (``zeta'') of the observer's security label, capturing the dependence of the terms' equivalence on the observer's label. \para{Logical relations} Figure~\ref{fig:logical} shows the complete definition of the logical relation. We use the notation \Relgx\ to denote two related substitutions, $\Relex\Tt$ to denote two related computations, and $\Relvx\Tt$ to denote two related values. They are parameterized by a type \Tt, an acts-for hierarchy \Ahi\ and an upper-bound \Rell\ of the observer's security label. By R-Subs, two substitutions are related at environment \Eenv\ if \Eenv\ is closed and if the substitutions assign all variables in environment \Eenv\ to related values. R-Term indicates that two terms are related at type \Tt\ if they both have type \Tt\, and if they evaluate to values which are related at type \Tt. R-Label is the crucial definition for logical relations with labels. It relates {\em any} two values at type \Tuly\ as long as the label \Lt\ is not lower than the observer's label \Rell. If R-Label does not apply, values are related only by one of the following syntax-directed rules. By R-Unit, \Eunit\ is related only to itself and, similarly, by R-PName, \Epx\ is related only to itself (because they are both singleton types). R-Inl says that two values are related at \Tsuml\Tta\Ttb\ if they both are left-injections of the form \Einlx\Vt\ and \Einlx\Vtp, and if \Vt\ and \Vtp\ are related at \Tt. By R-Fun, two values are related at \Tfunl\Tta\Ttb\ if their applications to {\em all} values related at \Tta\ are related at \join\Ttb\Lt. Lastly, R-All indicates that two values are related at \Tallxpl\Tt\ if their instantiations with {\em all} principals acting for \Lp{} are related at \join\Tt\Lt. Using these definitions, we strengthen the induction hypothesis of noninterference so that the theorem follows as a special case of this substitution lemma. In essence, the lemma states that substitution of related values yields related results. \begin{lem}[Substitution for logical relations]\label{lem:subs-logical} \ \\ If\/ $\Typex\Et\Tt$, $\Pmodx$, $\Ahi=\Psx\Penv$ and $\Relg\Es\Esp\Rell{\Psx\Eenv}$, then \(\Reley{\Epsx\Et}{\Epsxp\Et}{\Psx\Tt}\). \end{lem} \begin{proof} We only give a proof sketch here; a complete proof can be found in Appendix. By Lemma~\ref{lem:subs-sub}, the terms $\Epsx\Et$ and $\Epsxp\Et$ are well-typed. It remains to show that $\Evalmx{\Epsx\Et}\Vt$ and $\Evalmx{\Epsxp\Etp}\Vtp$ and $\Relvx{\Psx\Tt}$, which we prove by induction on the typing derivations: For T-PName, the result follows by R-PName because $\Epsx\Et=\Epsxp\Et=\Epx$ and $\Psx{\Tpl\Lx}=\Tul{(\Tp\Lx)}{\Psx\Lt}$. For T-IfDel, the two terms in the condition are related by the induction hypothesis. By inversion, either $\Ahi\proves\Lt\not\sle\Rell$ or they are both related using R-PName. In the former the result follows trivially by R-Label. In the latter, the test conditions evaluate to $\Ep\Lxa$ and $\Ep\Lxb$. Then, both terms step to the same branch depending on whether $\Ahi\proves\Lxa\delto\Lxb$. The result follows because both branches are related by the induction hypothesis. For T-All, $\Epsx{\Eallx\Lp\Etz}$ evaluates to $\Eall\Lv{\Psx\Lp}{\Epsx\Etz}$ while $\Epsxp{\Eallx\Lp\Etz}$ evaluates to $\Eall\Lv{\Psx\Lp}{\Epsxp\Etz}$. It remains to show that $\forall(\Actsfora\Lx{\Psx\Lp})$: % \[\begin{array}{rcl} \Ahi &\proves& {(\Epapp{(\Eall\Lv{\Psx\Lp}{\Epsx\Etz})}\Lx)} \\ && \approx_\Rell {(\Epapp{(\Eall\Lv{\Psx\Lp}{\Epsxp\Etz})}\Lx)} : {\Psx{\join\Ttz\Lt}} \end{array}\] % By E-PAppAll, these two applications step to $\Subs\Lv\Lx{\Epsx\Etz}=\Es\Psxz\Etz$ and $\Subs\Lv\Lx{\Epsxp\Etz}=\Esp\Psxz\Etz$, where $\Psz=\Ps,\Lv\mapsto\Lx$. The result follows by the induction hypothesis because $\Mod\Psz{\Penv,\Lv\delto\Lp}$. For T-PApp, the two terms on the left are related by the induction hypothesis. The two principals on the right are both $\Psx\Lpa$ and, by $\ActsforD\Lpa\Lpb$ and Lemma~\ref{lem:subs-sub}, we have $\Actsfora{\Psx\Lpa}{\Psx\Lpb}$. The result then follows by the definition of R-All. For T-Sub, the result follows by Lemma~\ref{lem:subs-sub} and the following properties of subtyping with respect to logical relations (which can be proved by induction on the subtyping derivations): (1) If $\Reley\Et\Etp\Tt$ and $\Stypea\Tt\Ttp$, then $\Reley\Et\Etp\Ttp$. (2) If $\Relv\Vt\Vtp\Tt$ and $\Stypea\Tt\Ttp$, then $\Relv\Vt\Vtp\Ttp$. \end{proof} \section{Declassification and authority} \label{sec:declassify} %% Cite robust declassification papers. Although noninterference is useful as an idealized security policy, in practice most programs \textit{do} intentionally release some confidential information. This section considers the interaction between run-time principals and declassification and suggests \textit{run-time authority} as a practical approach to delimiting the effects of downgrading. The basic idea of declassification is to add an explicit method for the programmer to allow information flows downward in the security lattice. The expression \Edcls\Et\Tt{} indicates that \Et\ should be considered to have type \Tt, which may relax some of the labels constraining \Et. Declassification is like a type-cast operation; operationally it has no run-time effect: \[ \Evalx{\Edcls\Et\Tt}{\Et}\quad\mbox{(E-Dcls)} \] One key issue is how to constrain its use so that the declassification correctly implements a desired security policy. Ideally, each declassification would be accompanied by formal justification of why its use does not permit unwanted downward information flows. However, such a general approach reduces to proving that a program satisfies an arbitrary policy, which is undecidable for realistic programs. An alternative is to give up on general-purpose declassification and instead build it into appropriate operations, such as encryption. Doing so essentially limits the security policies that can be expressed, which may be acceptable in some situations, but is not desirable for general-purpose information-flow type systems. To resolve these tensions, the original decentralized label model proposed the use of \textit{authority} to scope the use of declassification. Intuitively, if \Alice{} is an owner of the data, then her authority is needed to relax the restrictions on its use. For example, to declassify data labeled \lbl{\policy{\Alice}{}}{} to permit \Bob{} as a reader (i.e. relax the label to \lbl{\policy{\Alice}{\Bob}}{}) requires \Alice{}'s permission. In the original DLM, a principal's authority is statically granted to a piece of code. Zdancewic and Myers proposed a refinement of the DLM authority model called \textit{robust declassification}~\cite{ZM01,Zda03}. Intuitively, robust declassification requires that the \textit{decision} to release the confidential data be trusted by the principals whose policies are relaxed. In a programming language setting, robustness entails an \textit{integrity} constraint on the program-counter (\pc{}) label---the \pc{} label is a security label associated with each program point; it approximates the information that may be learned by observing that the program execution has reached the program point. For example, suppose that the variable $x$ has type \Tul{\Tbool}{\Lt} then the \pc{} label at the program points at the start of the branches $v_0$ and $v_1$ of the conditional expression \Ecase{x}{v_0}{v_1} satisfies $l \sle \pc{}$ because the branch taken depends on $x$---observing that the program counter has reached $v_0$ reveals that $x$ is \TRUE{}. If $x$ has low integrity, for example, if it is untrusted by \Alice{}, then $l \sle \pc{}$ implies that the integrity of the \pc{} labels in the branches are also untrusted by \Alice{}. Robustness requires that \Alice{} trusts the \pc{} at the point of her declassification; even if she has granted her authority to this program, no declassification affecting her policies will be permitted to take place in $v_0$ or $v_1$. In the presence of run-time principals, however, the story is not so straightforward. To adopt the authority model, we must find a way to represent a run-time principal's authority. Similarly, to enforce robust declassification, we must ensure that at runtime the integrity of the program counter is trusted by any run-time principals whose data is declassified. At the same time, we would like to ensure backward compatibility with the static notions of authority and robustness in previous work~\cite{ZM01,Zda03}. \subsection{Run-time authority and capabilities} To address downgrading with run-time principals, we use \textit{capabilities} (unforgeable tokens) to represent the run-time authority of a principal. The meta-variable $i$ ranges over a set of \textit{privilege identifiers} \I{}. We are interested in controlling the use of declassification, so we assume that \I{} contains at least the identifier \DECLASSIFY{}, but the framework is general enough to control arbitrary privileges. Below, we consider using capabilities to regulate other privileged operations, such as delegation. \begin{figure*} \begin{minipage}[t]{2.2in} \[\begin{array}{rll|} \Tu & ::= \ldots & \mbox{Base types} \\ &\Tfpc\Pc\Tt\Tt & \quad\mbox{function} \\ & \Tc & \quad\mbox{capability} \\ \Pc & ::= \Opt{\Pc,\Lp\grant\Eo} & \mbox{Authority} \end{array}\] \end{minipage} \begin{minipage}[t]{2.3in} \[\begin{array}{rll} \Et & ::= \ldots& \mbox{Terms} \\ & \Eifgranti\Et\Et\Et\Et & \quad\mbox{if certify}\\ & \Edcls\Et\Tt & \quad\mbox{declassify}\\ & \ %% && \Edlg\Et\Et & \quad\mbox{delegate}\\ \end{array}\] \end{minipage} \begin{minipage}[t]{1.8in} \[\begin{array}{|rll} \Vt & ::= \ldots& \mbox{Values} \\ & \Eqx & \quad\mbox{capability}\\ \\ \multicolumn{2}{|c}{i \in \I{}} & \mbox{Privileges} \end{array}\] \end{minipage} \caption{\lang{} with run-time authority} \label{fig:authority} \end{figure*} Figure~\ref{fig:authority} summarizes the changes to the language needed to support run-time authority. Just as we separate the static principal names from their run-time representation, we separate the static authority granted by a principal from its representation. The former, static authority, is written $\Lp\grant\Eo$ to indicate that principal \Lp{} grants permission for the program to use privilege \Eo{}. For example, a program needs to have the authority $\Alice\grant\DECLASSIFY{}$ to declassify on \Alice{}'s behalf. The latter, run-time authority, is written \Eqx{} and represents an unforgeable capability created by principal \Lx{} and authorizing privilege $i$. Capabilities have static type \Tc{}. A program can test a capability at run time to determine whether a principal has granted it privilege $i$ using the expression \Eifgranti{e_1}{e_2}{e_3}{e_4}. Here, $e_1$ evaluates to a capability and $e_2$ evaluates to a run-time principal; if the capability implies that the principal permits $i$ the first branch $e_3$ is taken, otherwise $e_4$ is taken. To retain the benefits of robust declassification, we generalize the \pc{} label to be a set of static permissions, \Pc{}. The function type constructor must also be extended to indicate a bound on the calling context's \pc{}. In our setting, the bound is the minimum authority needed to invoke the function. We write such types as \Tfpc{\Pc}{\Tta}{\Ttb}. For example, if $f$ has type \Tfpc{\Alice\grant\DECLASSIFY}{\Tul{\Tbool}{\lbl{\policy{\Alice}{}}{}}}{\Tul{\Tbool}{\Botlbl}} then the caller of $f$ must have \Alice{}'s authority to declassify---$f$ may internally do some declassification of data owned by \Alice{}. Therefore $f$, which takes data owned by \Alice{} and returns public data, may reveal information about its argument. On the other hand, a function of type \Tfpc{\Alice\grant\DECLASSIFY}{\Tul{\Tbool}{\lbl{\policy{\Bob}{}}{}}}{\Tul{\Tbool}{\Botlbl}} cannot declassify the argument, which is owned by \Bob{}, unless \Alice{} acts for \Bob{}. Note that the types accurately describe the security-relevant operations that may be performed by the function. The examples above use only static authority. To illustrate how run-time capabilities are used, consider this program: \[\begin{array}{rcl} h & : & \TallS\alpha {[\cdot]\; \Tp{\alpha} \rightarrow [\cdot]\; \Tc \rightarrow [\cdot]\; \Tul{\Tbool}{\lbl{\policy{\alpha}{}}{}} \rightarrow {\Tul{\Tbool}{\Botlbl}}} \\ % h & = & \EallS{\alpha}{}{} \lambda \name{user}\ty\Tp{\alpha}.\; \lambda \name{cap}\ty\Tc.\; \lambda \name{data}\ty\Tul{\Tbool} {\lbl{\policy{\alpha}{}}{}}.\; \\ % & & \quad \Eifgrant{\name{cap}}{\name{user}}{\DECLASSIFY}{}{} \\ && \qquad{(\Edcls{\name{data}}{\Tul{\Tbool}{\Botlbl}})}\;{\FALSE} \end{array} \] % The type of $h$ is parameterized by a principal $\alpha$, and the authority constraint $[\cdot]$ indicates that no static authority is needed to call this function. Instead, $h$ takes a run-time principal \name{user} (whose static name is $\alpha$), a capability \name{cap}, and some data private to $\alpha$. The body of the function tests whether capability \name{cap} provides evidence that \name{user} has granted the program the \DECLASSIFY{} privilege. If so, the first branch is taken and the data is declassified to the bottom label. Otherwise $h$ simply returns \FALSE{}. The program $h$ illustrates the use of the \Edcls{e}{t} expression, which declassifies the expression $e$ of type $t'$ to have type $t$, where $t'$ and $t$ differ only in their security label annotations. The judgment $\Penv \proves t_1 - t_2 = \Ls$ indicates that under the principal hierarchy $\Penv$, the type $t_1$ may be declassified to type $t_2$ using the authority of the principals in \Ls{}. We call \Ls\ the set of declassification requisites. For example, $\proves \Tul{\Tbool}{\lbl{\policy{\Alice}{}}{}} - \Tul{\Tbool}{\lbl{\policy{\Alice}{\Bob}}{}} = \brackets\Alice$, because \Alice{}'s authority is needed to add \Bob{} as a reader. This judgment is used when typechecking the \DECLASSIFY\ expression: \[ \Rule{ \begin{array}[c]{l} \Penv;\Eenv;\Pc\proves\Et:\Ttb \\ \Penv\proves \Ttb-\Tta = \Ls \\ \ActsforD\Ls{\Pc(\Cd{declassify})} \end{array}} {\Penv;\Eenv;\Pc\proves{\Edcls\Et\Tta}:\Tta} \;\;\rulelabel{(T-Dcls)} \] The typing judgments for run-time authority are of the form $\Penv;\Eenv;\Pc\proves\Et:\Tt$, where \Pc{} is the set of static capabilities available within the expression \Et. Given static capabilities \Pc{}, we write $\Pc(i)$ for the set of principals that have granted the permission $i$; so $\Pc(i) = \{p \sep p\grant{}i \in \Pc\}$. In the rule T-Dcls, $s$ is the set of principals whose authority is needed to perform the declassification, therefore the condition $\Penv \proves s \delto \Pc(\DECLASSIFY)$ says that the set of \DECLASSIFY{}-granting principals in the static authority is sufficient to act for $s$. For robustness, we must ensure that the integrity of the data is reflected in the set of static capabilities available. To do so, we define an operator $\Pc|l$, that restricts the capabilities in \Pc{} to just those whose owners have delegated to principals present in the integrity portion of the label $l$. With respect to hierarchy \D{}, the formal definition is: \[\Pc|\lbl{d}{s} = \{p\grant i \in \Pc \sep \exists q \in s.\; \D \proves p \delto q\}\] The restriction operator occurs in the typing rules of branching constructs. For example, this is the modified form of the \Cd{case} expression: % \[\Rule{ \begin{array}{l} \Penv;\Eenv;\Pca\proves\Et:{\Tsuml\Tta\Ttb} \\ \Penv;\Eenv;\Pca|l \proves \Vta:{\Tfpcl\Pcb\Tta\Tt} \\ \Penv;\Eenv;\Pca|l \proves \Vtb:{\Tfpcl\Pcb\Ttb\Tt} \\ \D \proves\Pcb\delto{(\Pca|\Lt)} \end{array}} {\Penv;\Eenv;\Pca\proves{\Ecase\Et\Vta\Vtb}:{\join\Tt\Lt}} \;\;\rulelabel{(T-Case)} \] The rule for capability certification also uses the restriction operator, but it also adds the permission $p \grant i$ before checking the branch taken when the capability provides privilege $i$ (\Etc\ below): % \[ \Rule{ \begin{array}{l} \Penv;\Eenv;\Pc\proves\Eta:{\Tul{\Tc}\Lt} \\ \Penv;\Eenv;\Pc\proves\Etb:{\Tpl\Lp} \\ \Penv;\Eenv;(\Pc,\Lp\grant i)|\Lt\proves\Etc:\Tt \\ \Penv;\Eenv;\Pc|\Lt\proves\Etd:\Tt \end{array}} {\Penv;\Eenv;\Pc\proves{\Eifgranti\Eta\Etb\Etc\Etd}:{\join\Tt\Lt}} \;\;\rulelabel{(T-IfCert)} \\ \] % Note that the restriction is applied \textit{after} the permission is added, to prevent the specious amplification of rights based on untrustworthy capabilities. At run time, the validity of a capability under the current acts-for hierarchy determines which branch of the certification expression is taken: % \[ \Rule{\Ahi\proves{\Eq\Lxa\Eo}\certify{\Ep\Lxb}\grant\Eo} {\Evalx{\Eifgranti{\Eq\Lxa\Eo}{\Ep\Lxb}\Etc\Etd}\Etc} \;\;\rulelabel{(E-CertYes)} \] \[ \Rule{\Ahi\proves{\Eq\Lxa\Eo}\not\certify{\Ep\Lxb}\grant\Eo} {\Evalx{\Eifgranti{\Eq\Lxa\Eo}{\Ep\Lxb}\Etc\Etd}\Etd} \;\;\rulelabel{(E-CertNo)} \] % To verify that a capability grants permission for principal \Lxb{} to perform some privileged operation $i$, the run-time system determines whether the issuer \Lxa{} of the capability acts for the principal \Lxb{} wanting to use the capability: If \(\Ahi\proves\Lxb\delto\Lxa\) then \(\Ahi\proves{\Eq\Lxa\Eo}\certify{\Ep\Lxb}\grant\Eo\). Function types capture the static capabilities that may be used in the body of the function, and the modified rule for typechecking function application requires that the static capabilities \Pc{} of the calling context are sufficient to invoke the function: \[ \Rule{\Penv;\Eenv,\Ev:\Tta;\Pc \proves \Et:\Ttb & \LabelD{\Lt}} {\Penv;\Eenv;\Empty \proves{\Efunx\Tta\Et}:{\Tfpcl\Pc\Tta\Ttb}} \;\;\rulelabel{(T-Fun)} \] \[ \Rule{ \begin{array}{l} \Penv;\Eenv;\Pca\proves \Eta:{\Tfpcl\Pcb\Tta\Ttb} \\ \Penv;\Eenv;\Pca\proves \Etb:\Tta \quad \D \proves \Pcb \delto (\Pca|\Lt) \end{array}} {\Penv;\Eenv;\Pca\proves {\Eapp\Eta\Etb}:{\join\Ttb\Lt}} \;\;\rulelabel{(T-App)} \] Finer-grained control of declassification can be incorporated into this framework by refining the \DECLASSIFY{} privilege identifier with more information, for instance to give upper bounds on the data that may be declassified or distinguish between declassify expressions applied for different reasons (see Section~\ref{sec:eg}). %% One appealing feature of this language design is that the type system %% makes tradeoffs between static versus run-time control of authority %% (and hence declassification) explicit. \subsection{Delegation} \label{sec:delegate} Delegation allows the acts-for hierarchy to change during program execution---so far, the operational semantics have been given in terms of a fixed \Ahi{}. When $p$ delegates to $q$, then $q$ may read or declassify all data readable or owned by $p$; therefore, delegation is a very powerful operation that should require $p$'s permission. We add a new expression \Edel\Eta\Etb\Etc{} that allows programmers to extend the acts-for hierarchy in the scope of the expression \Etc{}. Here, \Eta{} and \Etb{} must evaluate to run-time principals. Assuming their static names are $p$ and $q$, respectively, the body \Etc{} is checked with the additional assumption that $p \delto q$. Because delegation is a privileged operation, it needs the static authority of principal $p$. We extend the set of privileges \I{} to include additional identifiers of the form $\Cd{delegate}_{\Lp\delto\Lq}$. The constraint $\ActsforD\Lp{\Pc(\Cd{delegate}_{\Lp\delto\Lq})}$ ensures that the capability to extend the acts-for hierarchy has been granted by $p$: \[ \Rule{ \begin{array}{l} \Typep\Eta{\Tulx{(\Tp\Lp)}} \\ \Typep\Etb{\Tpl\Lq} \\ \PType{\Penv,\Lp\delto\Lq}\Eenv\Etc\Tt \\ \ActsforD\Lp{\Pc(\Cd{delegate}_{\Lp\delto\Lq})} \end{array}} {\Typep{\Edel\Eta\Etb\Etc}{\join\Tt\Lt}} \;\;\rulelabel{(T-LetDel)} \] As shown by the following evaluation rule E-LetDel, the body of a let-delegation term is evaluated to a value under the extended acts-for hierarchy, but the original acts-for hierarchy is restored afterwards. This ensures that the delegation is local to $\Etc$: % \[ \Rule{(\Ahi,\Lxa\delto\Lxb),\Etc\eval(\Ahi,\Lxa\delto\Lxb),\Etcp} {\Evalx{\Edel{\Ep\Lxa}{\Ep\Lxb}\Etc}{\Edel{\Ep\Lxa}{\Ep\Lxb}\Etcp}} \] \subsection{Acquiring capabilities} %% Motivate capabilities as first-class things. Describe the grant %% operation. %% Explain delegation. %% Consider revocation. \cite{Jim01,GJ00} So far, this paper has not addressed how capability objects are obtained by the running program. Because capabilities represent privileges conferred to the program by run-time principals, they must be provided by the run-time system---they represent part of the dynamic execution environment. In practice, capabilities may be created in a variety of ways: The operating system may create an appropriate set of capabilities after authenticating a user. If the capabilities are implemented via digital certificates, then they may be obtained over the network using the underlying PKI. Capabilities may also be generated by the system in response to user input, for instance after prompting for user confirmation via a secure terminal. To hide the details of the mechanism for producing capabilities, we model the external environment as a black box \E{} and write $\E \proves \Eq\Lx\Eo$ to indicate that environment \E{} produces the capability \Eq\Lx\Eo{}. Using the expression \Egrant\Et\Eo{}, where \Et{} evaluates to a run-time principal, the program can query the environment to see whether a given capability is available. This operation either returns the corresponding capability object \Eq\Lx\Eo{} or indicates failure by returning \Eunit{}. This behavior is captured by the following typechecking and evaluation rules (E-AcqNo, not shown, steps to \Einr\Tt\Eunit{} when $\E\not\proves{\Eq\Lx\Eo}$): % \[ \Rule{\Typep\Et{\Tulx{(\Tp\Lp)}}} {\Typep{\Egrant\Et\Eo}{\Tulx{(\Tsum{\Tulx\Tc}\Tunitlx)}}} \;\;\rulelabel{(T-Acq)} \] \[ \Rule{\E\proves{\Eq\Lx\Eo}} {\Evalx{\Egrant{\Ep\Lx}\Eo}{\Einl\Tt{\Eq\Lx\Eo}}} \;\;\rulelabel{(E-AcqYes)} %% & %% \Rule{\E\not\proves{\Eq\Lx\Eo}} %% {\Evalx{\Egrant{\Ep\Lx}\Eo}{\Einr\Tt\Eunit}} %% \rulelabel{(E-AcqNo)} \] A common programming idiom is to obtain a run-time capability using \GRANT{}, certify the capability, and, if both checks succeed, act using the newly acquired abilities: % \[\begin{array}{l} \Cd{case}\ (\Egrant{\name{user}}{\DECLASSIFY}) \\ \quad \lam{\name{cap}\ty\Tc}{} \ \Eifgrant{\name{cap}}{\name{user}}{\DECLASSIFY}{}\\ \qquad (\Edcls{\name{data}}{t})\;(\ldots) \\ \quad \lam{\name{x}\ty \Tunit}{\ldots} \end{array}\] When written in this way, there appears to be a lot of redundancy in these constructs. However, for the sake of modularity and flexibility, we separate the introduction of a capability (\GRANT{}) from its validation (the \IF{} test) and the use of the conferred privileges (the \DECLASSIFY{}). A surface language like Jif, would provide syntactic sugar that combines the first two, the last two, or even all three of these operations. Treating these features independently also allows more flexibility for the programmer. For instance, the ability to pass capabilities as a first class objects is important in distributed settings, where one host may manufacture a capability and send it to a second host that can verify the capability and act using the privileges (see Section~\ref{sec:eg}). % Note that it is never necessary to manipulate private keys % directly---only privileges signed by public keys are needed. This is % compatible with the intuition that a private key should never be % disclosed. \subsection{Soundness} As a second theoretical contribution of this paper, we have extended the soundness result (Theorem~\ref{thm-sound}) in Section~\ref{sec:basic} to the full language with authority and capability as follows. A complete proof can be found in Appendix. \begin{thm}[Soundness] (1) Progress: If $\Typeb\Et\Tt$, then $\Et=\Vt$ or $\Evalx\Et\Etp$. (2) Preservation: If $\Typeb\Et\Tt$ and $\Evalx\Et\Etp$, then $\Typec\Etp\Tt$ such that $\Ahi\delto\Ahi'$ and $\Pc\delto\Pc'$. \end{thm} We have not proved a noninterference result for \lang{} with the run-time authority because we are primarily concerned with regulating declassification, which intentionally breaks noninterference. We conjecture that well-typed programs not containing \DECLASSIFY{} or delegation satisfy noninterference following a similar argument to that given in Section~\ref{sec:noninterference}, but we leave the proof of this claim to future work. \section{PKI and application} \label{sec:pki} \subsection{Public key infrastructure} %% Question: How do you resolve the DLM's principal hierarchy with the %% notion of an acts-for relation? Doesn't the acts-for relation have %% to be globally consistent? Or is the acts-for relation defined in %% terms of locally available delegation assertions? (??) %% Can you add a new primitive to Jif that allows the acts-for %% hierarchy to be changed at runtime? Currently Jif allows the %% acts-for hierarchy to be queried at runtime, and there is an %% assumption that the hierarchy changes with a frequency less than %% the time needed to execute the block of code in the acts-for. (In %% some sense, this says that the actsFor {...} construct acquires a %% lock on the hierarchy), making it a kind of transaction mechanism.) %% But the current decentralized label model doesn't support a means %% of adding a new relation to the acts-for hierarchy at runtime. %% This could be another operation, like declassification, that must %% be carefully regulated (and hence needs to be robust?) %% If you do add such a thing, do you have to worry about revoking the %% edge in the acts-for hierarchy? Also, what is the intended scope of %% the acts-for hierarchy? If it is global, then doesn't it imply that %% the decentralized label model isn't really ``decentralized''? This section considers some possible implementations of run-time principals, concentrating on one interpretation in terms of a public key infrastructure. If run-time principals are added to an information-flow type system whose programs are intended to run within a single, trusted execution environment, the implementation is straightforward: The trusted run time maintains an immutable (and persistent) mapping of principal names to unique identifiers, the acts-for hierarchy is a directed graph with nodes labeled by identifiers, and capabilities can be implemented as (unforgeable) handles to data structures created by the run-time system---this is the strategy currently taken by Jif. If the programs are intended to run in a distributed setting, the implementation becomes more challenging. Fortunately, the appropriate machinery (principal names, delegation, and capabilities) has already been developed using public-key cryptography~\cite{HK00,GM90}. We can interpret \lang{} in terms of PKI as follows: run-time principals are implemented via public keys, the acts-for hierarchy is implemented via certificate chains, and capabilities are implemented as digitally signed certificates. Formally, we have the following interpretation, where \key\Lx{} is the public key corresponding to \Lx{} and \sign\Lx{\Interp\Eo} is a certificate signed using \Lx{}'s private key. The remaining constructs (the acts-for relation and the privileged operations) are interpreted as tuples: \[ \begin{array}{rcl} \Interp{\Epx} &=& \key\Lx \\ \Interp{\Epxa\delto\Epxb} &=& (\key\Lxa,\key\Lxb) \\ \Interp{\Eq\Lx\Eo} &=& \sign\Lx{\Interp\Eo} \\ \Interp{\Cd{declassify}} &=& \Cd{dcls} \\ \Interp{\Lx\grant\Eo} &=& (\key\Lx,\Interp\Eo) \\ \Interp{\Cd{delegate}_{\Lxa\delto\Lxb}} &=& (\Cd{del},\key\Lxa,\key\Lxb) \end{array} \] \[\Rule{(\key\Lxb,\key\Lxa) \in \Interp{\Ahi}^*} {\Ahi\proves\sign\Lxa{\Interp\Eo} \certify (\key\Lxb,{\Interp\Eo})} \] The interpretation of the acts-for hierarchy, $\Interp\Ahi{}^*$, is a binary relation on public keys---the reflexive, transitive closure of the pointwise interpretation of the delegation pairs. Given these definitions, it is clear how to interpret the capability verification---we use cryptographic primitives to verify that the digital certificate is signed by the corresponding public key: $\Cd{verify}\;\key\Lxa\; \sign\Lxa{\Interp\Eo}=\Interp\Eo$. Note that in case of reflexive acts-for, we have $\key\Lxa=\key\Lxb$ and ${\sign\Lxa{\Interp\Eo} \certify (\key\Lxa,{\Interp\Eo})}$. The implementation uses graph reachability to test for transitive acts-for relations in \Ahi. It is easy to show that the existence of a path in $\Interp{\Ahi}^*$ implies the existence of a valid certificate chain. Now the universally trusted host $\top{}$ behaves as a certificate authority that generates private keys and issues certificates binding principal names to their corresponding public keys. To satisfy the axiom $\D \proves X \delto \top$, we assume that each host's run-time is configured with \sign{X}{\Interp{X \delto \top}} and $(X, \top) \in \Interp{\Ahi}$ for each $X$---this information would be acquired by a host when it receives the principal $X$ to key \key{X} binding from the certificate authority. % , although it % may be possible to sensibly interpret private keys This interpretation permits flexibility in specifying security policies. Consider the following program that takes in two capabilities and some data owned by Alice and attempts to declassify it. % % \begin{verbatim} % (1) fun c1:C. c2:C. fun x:bool{Alice:!}. % (2) if (c1 => Alice |> delegate(Alice <= Bob)) % (3) let (Alice <= Bob) in % (4) if (c2 => Bob |> declassify) % (5) declassify x bool{!} % (6) ... % \end{verbatim} % \[ \begin{array}{cl} \mathcd{1} & \Efun{c_1}\Tc { \Efun{c_2}\Tc { \Efun{x}{\Tul\Tbool{\lbl{\Alice:}{}}}{}}} \\ \mathcd{2} & \quad \Eifgrant {c_1} \Alice {\Cd{delegate}_{\Alice\delto\Bob}}{} \\ \mathcd{3} & \quad\quad \Edel\Alice\Bob {} \\ \mathcd{4} & \quad\quad \Eifgrant {c_2} \Bob {\Cd{declassify}} {} \\ \mathcd{5} & \quad\quad \Edcls x {\Tul\Tbool{\lbl{}{}}} \\ \end{array} \] By the typing rule T-Dcls of declassification, line 5 needs the authority $p\,\grant\,\DECLASSIFY$ for some $p$ acting for \Alice{} because \Alice's policy is being weakened: \[\proves \Tul\Tbool{\lbl{\Alice:}{}} - \Tul\Tbool{\lbl{}{}} = \{\Alice\}\] The PKI implementation justifies the presence of \Alice{}'s authorization. Assume the acts-for hierarchy \Ahi\ at line 1 is the default hierarchy consisting of only $(X,\top)$ pairs. Line 2 uses $\Interp{\Alice} = \key\Alice$ to verify the certificate \( \Ahi\proves c_1\certify(\key\Alice,\Interp\Eo) \) where $\Interp\Eo={\Interp{\Alice\grant{\Cd{delegate} _{\Alice\delto\Bob}}}}=(\Cd{del},\key\Alice,\key\Bob)$. Since the acts-for hierarchy is otherwise empty, $c_1$ must be of the form \sign\Alice{\Interp\Eo} or \sign\top{\Interp\Eo}. The first certificate can be validated using only \key\Alice{}; the second can be validated starting from \key\Alice{} by checking the certificate chain $\sign{\Alice}{\Interp{\Alice \delto \top}} \chain\sign{\top}{\Interp{i}}$. If one of these chains is valid, line 3 adds the delegation information into the hierarchy so that $(\key\Alice,\key\Bob) \in \Interp{\Ahi}$. Similarly, there are two certificates $c_2$ that may justify the static condition \[\Alice\delto\Pc(\DECLASSIFY)=\Alice\delto\Bob\] required by rule T-Dcls. If $c_2=\sign\Bob{\Cd{dcls}}$, the static condition holds at runtime because we can find the chain: \[\sign{\Alice}{\Interp{\Alice \delto \Bob}} \chain \sign\Bob{\Cd{dcls}}\] If $c_2 = \sign{\top}{\Cd{dcls}}$ we can find the chain: {\small \[\sign{\Alice}{\Interp{\Alice \delto \Bob}} \chain \sign{\Bob}{\Interp{\Bob \delto \top}} \chain \sign\top{\Cd{dcls}}\]} In general, the justification for constraint $p_1 \delto \Pc(i)$ is the existence of some certificate chain of the form: {\small \[ \sign{p_1}{\Interp{p_1 \delto p_2}} \chain\ldots\chain \sign{p_{n-1}}{\Interp{p_{n-1} \delto p_n}} \chain \sign{p_n}{\Interp{i}} \] } % Alternatively, we can write Line 4 as $\Cd{if}\;({c_2}\certify\Alice % \grant{\Cd{declassify}})$ and still be able to pass either % $c_2=\sign\Alice{\Cd{dcls}}$ or $c_2=\sign\Bob{\Cd{dcls}}$. The % reasoning is similar to above. % If we put the verifications of delegation and declassification % together, it is clear how to justify the interpretation of V-Cert: we % first use \key\Alice\ to verify the delegation certificate and output % \key\Bob, then we use \key\Bob\ to verify the declassification % certificate. Here we do not use the acts-for hierarchy \Ahi\---the % hierarchy is used only to keep track of delegation information such % that delegation and privileged operations can be in different parts of % the program. % \[\Rule{\Ahi\proves\sign\Alice{\Cd{del},\key\Alice,\key\Bob} % \certify (\key\Alice,\key\Bob)} {\Ahi\proves\sign\Bob{\Cd{dcls}} % \certify (\key\Alice,\Cd{dcls})}\] %% In the existing Jif implementation, the run-time representation of a %% principal is a Java class located in a particular directory known to %% the Jif run-time environment. It seems plausible that the class file %% associated with a principal could contain the principal's public key %% and methods for verifying digital signatures. Therefore, we %% conjecture that the PKI interpretation of run-time principals outlined %% in this paper could be readily implemented. \subsection{Application to distributed banking} \label{sec:eg} \newcommand{\userid}{\Z{user_{id}}} \newcommand{\agentid}{\Z{agent_{id}}} \newcommand{\cdel}{\Z{c_{del}}} \newcommand{\creq}{\Z{c_{req}}} \newcommand{\crct}{\Z{c_{prt}}} \newcommand{\elet}{\Z{\Cd{let}\;}} \newcommand{\ein}{\Z{\;\Cd{in}}} \newcommand{\ecase}{\Z{\Cd{case}\;}} \newcommand{\Int}{\Z{\Cd{int}}} \newcommand{\ATM}{\Z{\name{ATM}}} \newcommand{\ATMk}{\Z{\name{ATM_j}}} \newcommand{\Bank}{\Z{\name{Bank}}} \newcommand{\withdraw}{\Z{\Cd{withdraw}_{100}}} \newcommand{\lbb}{\Z{\lbl{\policy\Bank\Bank}{}}} \newcommand{\lbbb}{\Z{\lbl{\policy\Bank\Bank}\Bank}} \newcommand{\lmm}{\Z{\lbl{\policy\ATMk\ATMk}{}}} \newcommand{\laa}{\Z{\lbl{\policy{agent}{agent}}{}}} \newcommand{\laaa}{\Z{\lbl{\policy{agent}{agent}}{agent}}} \newcommand{\luu}{\Z{\lbl{\policy{user}{user}}{}}} Figure~\ref{fig:example} shows a more elaborate example \lang{} program that implements a distributed banking scenario in which a customer interacts with their bank through an ATM. The example uses a number of standard constructs such as integers, pairs, let-binding, and existential types that are not in \lang{}, but could readily be added or encoded~\cite{Pie02}. The main functions for the ATMs and the \Bank{} are shown, along with the types of various auxiliary functions. \begin{figure*} \[\begin{array}{rcl} \renewcommand{\arraystretch}{0.5} ATM_j\_main &:& [\ATMk\grant\DECLASSIFY_{net}]\Tfun\Tunit\Tunit \\ Bank\_main &:& [Bank\grant\DECLASSIFY_{net}] \Tfun\Tunit\Tunit \\ request &:& \forall (agent,user).\; {\Tul{(\Tp{agent}, \Tp{user}, \Tc, \Tc)}{\lbb}} \rightarrow \Tul\Int{\laaa} \\ listen &:& \Tunit\rightarrow \exists (agent,user).\; \Tul{(\Tp{agent}, \Tp{user}, \Tc, \Tc, (\Tfun{\Tul{\Int}{\laa}}\Tunit))}{\lbbb} \\ login &:& \Tfun\Tunit{\Tul{(\exists user.\; \Tp{user} , \Tc)}{\lmm}} \\ print &:& \Tfun{\Int\lbl{}{}}\Tunit \\ get &:& \forall user.\; \Tfun{\Tp{user}}{\Tul{\Int}{\lbb}} \\ set &:& \forall user.\; \Tfun{\Tp{user}}{\Tfun\Int\Tunit} \end{array} \] \noindent \begin{minipage}[t]{3.9in} \[\begin{array}{l} ATM_j\_main = \lambda{x}:\Tunit. \\ \quad\elet[user,(\userid,\cdel)]\; = login\;\Eunit\ein \\ \quad\ecase(\Egrant\userid\withdraw) \\ \quad\quad\lambda\creq:\Tc.\; \elet message = [(agent,user), \\ \quad\quad\quad\quad(\ATMk,\userid,\cdel,\creq)]\ein \\ \quad\quad\quad\elet data = \DECLASSIFY_{net}\; message \\ \quad\quad\quad\quad \Tul{(\Tp{\ATMk}, \Tp{user}, \Tc, \Tc)}{\lbb}\;\ein \\ \quad\quad\quad\elet balance = request\;[\ATMk,user]\; data\ein \\ \quad\quad\quad\ecase(\Egrant\userid\DECLASSIFY_{prt}) \\ \quad\quad\quad\quad\lambda\crct:\Tc.\; \Eifgrant\crct\userid{\DECLASSIFY_{prt}}{} \\ \quad\quad\quad\quad\quad\elet data = \DECLASSIFY_{prt} \; balance\; \Tul{\Int}{\lbl{}{}}\ein \\ \quad\quad\quad\quad\quad print\; data \\ \quad\cdots\quad\mbox{\it // other banking options} \end{array}\] \end{minipage} \begin{minipage}[t]{3in} \[\begin{array}{l} Bank\_main = \lambda{x}:\Tunit. \\ \quad\elet [(agent,user),(\agentid,\userid, \\ \quad\quad \cdel,\creq,reply)] = listen\;\Eunit\ein \\ \quad\Eifgrant\cdel\userid{\Cd{delegate}_{user \delto agent}} {} \\ \quad\quad\elet(\userid\delto\agentid)\ein \\ \quad\quad\Eifgrant\cdel\userid\withdraw {} \\ \quad\quad\quad\elet old = get\; [user]\; \userid\ein \\ \quad\quad\quad\elet balance = old - 100\ein \\ \quad\quad\quad set\;[user]\; \userid\; balance; \\ \quad\quad\quad\elet data = \DECLASSIFY_{net}\; \\ \quad\quad\quad\quad balance\;\Tul{\Int}{\luu}\ein \\ \quad\quad\quad reply\; data \\ \quad\cdots\quad\mbox{\it // other banking options} \end{array}\] \end{minipage} \caption{A distributed banking example} \label{fig:example} \end{figure*} The static principals are \Bank{} and $\name{ATM_1}$ through $\name{ATM_n}$, and there are two run-time principals, $user$ and $agent$. The principal $user$ is the customer at an ATM; $agent$ is the \Bank{}'s name for one of the $n$ ATMs that may connect to the bank server. On the left is the client code for \ATMk\ (a particular ATM), on the right is the bank server code. At the \ATMk, the customer logs in with the bank card and the password, revealing his identity $[user,\userid]$ and allowing \ATMk{} to act for him (represented by the capability \cdel). Then \ATMk\ interacts with $user$ to obtain his request such as withdrawing \$100. This interaction is modeled by the \Cd{acquire}. The ATM client packs the identities \ATMk\ and \userid\ and the delegation \cdel\ and the request \creq\ certificates into a message. To send the message over the channel to \Bank, \ATMk\ gives up the ownership of the data by declassifying the message to have label \lbb. As a result of the transaction with the bank server, \ATMk\ obtains the new account balance of the customer. Finally, \ATMk\ prompts to determine whether the $user$ wants a receipt, which requires a declassification certificate to print. This example makes use of fine-grained \DECLASSIFY{} privileges to distinguish between the printing and network send uses of declassification. The bank server listens over the private channel and receives the message. The $listen$ function also provides a $reply$ channel so that the balance can be returned to the same ATM. The server determines that $user$ has logged in to \ATMk{} by verifying \cdel{}, and if so, checks that the request capability is valid. If so, the server updates its database, and declassifies the resulting balance to be sent back to the ATM. In practice \Bank\ will also want to log the certificates for auditing purposes. In the functions $request$ and $listen$, we assume the existence of a private network between \ATMk\ and \Bank, which can be established using authentication and encryption. Since the network is private, the outgoing data must be readable only by the receiver; and, since the network is trusted, the incoming data has the integrity of the receiver. The labels of their types faithfully reflect this policy: for example, \lbb\ vs. \laaa\ in the type of $request$. Note the run-time authority for declassification and delegation are provided by the customer---they are acquired by the interaction of \ATMk\ and $user$. In contrast, in the types of $ATM_j\_main$ and $Bank\_main$, the static capability requirements $[\ATMk\grant\DECLASSIFY_{net}]$ and $[\Bank\grant\DECLASSIFY_{net}]$ indicate that the authorities to declassify to the network must be established from the caller. \section{Discussion} \label{sec:related} \subsection{Related work} The work nearest to ours is the Jif project, by Myers et al.~\cite{jif}. Although the Jif compiler supports run-time principals, its type system has not been shown to be sound. Our noninterference proof for \lang{} is a step in that direction. Jif also supports \textit{run-time labels}---run-time representations of the label annotations and a \cd{switch label} construct that lets programs inspect the labels at runtime. Although it is desirable to support both run-time labels and run-time principals, the two features are mostly orthogonal. % \footnote{In some cases % at runtime checking the acts-for relation between two principals % may imply some relation between labels or vice-versa.} Although the core \lang{} presented here is not immediately suitable for use by programmers (more palatable syntax would be needed), \lang{} can serve as a typed intermediate representations for languages like Jif. Moreover, this approach improves on the current implementation of the decentralized label model (DLM) because Jif does not support declassification of data owned by run-time principals, nor does it provide language support for altering the acts-for hierarchy. Our separation of static principals from their run-time representations also clarifies the type checking rules. The ability to perform acts-for tests at runtime is closely related to \textit{intensional type analysis}, which permits programs to inspect the structure of types at runtime. Our use of singleton types like \Tpx{} to tie run-time tests to static types follows the work by Crary, Weirich, and Morrisett~\cite{CWM02}. Static capability sets \Pc{} in our type system are a form of \textit{effects}~\cite{JG91}, which have also been used to regulate the read and write privileges in type systems for memory management~\cite{CWM99}. %% S&P related work %McLean~\cite{McL88,McL90,McL94} Mantel~\cite{Man00,Man00b} %% more related work The robustness condition on the set of run-time capabilities is very closely related to Java's stack inspection model~\cite{WF98,WAF00,FG02,pottier01esop}. In particular, the {\em enable-privilege} operation corresponds to our \Eifgranti\Eta\Etb\Etc\Etd{} and the check-privileges operation corresponds to the constraint on \Pc{} in the \DECLASSIFY{} rule. The restriction $\Pc{}|l$ of capability sets in the type-checking rule for function application corresponds to the taking the intersection of privilege sets in these type systems. However, stack inspection is {\em not} robust in the sense that data returned from an untrusted context can influence the outcome of privileged operations~\cite{FG02}. In contrast, \lang{} tracks the integrity of data and restricts the capability sets according to the principals' trust in the data---this is why the restriction $\Pc{}|l$ appears in the typechecking rule for \Cd{case} expressions. Banerjee and Naumann \cite{BN03} have previously shown how to mix stack inspection-style access control with information-flow analysis. They prove a noninterference result, which extends their earlier work on information-flow in Java-like languages~\cite{BN02}. Unlike their work, this paper considers run-time principals as well as run-time access control checks. Incorporating the principals used by the DLM into the privileges checked by stack inspection allows our type system to connect the information-flow policies to the access control policy, as seen in the typechecking rule for \DECLASSIFY{}. %% PKI? We have proposed the use of public key infrastructure as a natural way to implement the authority needed to regulate declassification in the presence of run-time principals. Although the interpretation of principals as public keys and authorized actions as digitally signed certificates is not new, integrating these features in a language with static guarantees brings new insights to information-flow type systems. This approach should facilitate the development of software that interfaces with existing access-control mechanisms in distributed systems~\cite{HK00,GM90}. Making the connection between PKI and the label model more explicit may have additional benefits. Myers and Liskov observed that the DLM acts-for relation is closely related to the speaks-for relation in the logical formulation of distributed access control by Abadi et al.~\cite{ABLP93}. Adopting the local names of the SDSI/SPKI framework~\cite{Aba98} may extend the analogy even further. Chothia et al.~also use PKI to model typed cryptographic operations for distributed access control~\cite{chothia03csfw}. Lastly, although capabilities mechanism in \lang{} provides facilities for programming with static and run-time capabilities, we do not address the problem of \textit{revocation}. It would be useful to find suitable language support for handling revocation, such as the work by Jim and Gunter~\cite{Jim01,GJ00}, but we leave such pursuits to future work. %% We have proposed the use of public key infrastructure as a natural way %% to implement the run-time authority %% -- Abadi et al %% -- SPKI %% Extend the notion of principals to include more structure, i.e. p's q %% - future work: Integrate authentication mechanisms more fully into the %% language so that the type information provided by run-time principals %% can reflect run-time authentication. Interesting related results along %% these lines includes the work on Cryptic by Jeffrey and %% Gordon~\cite{GJ01,GJ02?}. %% or conjunction principals $p \AND q$ (already encodable in Jif: %% $\mathcd{\{p:d; q:d\}} \equiv \mathcd{\{p\AND{}q:d\}}$) or disjunction %% principals $p \OR q$ --- not sure what these would mean. %\section{Discussion} %% \subsection{Scaling up the language} %% - Interaction with state %% - Discussion section about existential types (to implement %% Runtime.getUser()). %% - Interaction with other language features? (i.e. run-time labels) %% - future work: (bounded?) quantification over authority %% - future work: figure out the right theorems to prove about the %% relationship between declassification, run-time principals, and %% run-time authority. \subsection{Conclusions} Information-flow type systems are a promising way to provide strong confidentiality and integrity guarantees. However, their practicality depends on their ability to interface with external security mechanisms, such as the access controls and authentication features provided by an operating system. Previous work has established noninterference only for information-flow policies that are determined at compile time, but such static approaches are not suitable for integration with run-time security environments. This paper addresses this problem in three ways: (1) We prove noninterference for an information-flow type system with run-time principals, which allow security policies to depend on the run-time identity of users. (2) We show how to soundly extend this language with a robust access-control mechanism, a generalization of stack inspection, that can be used to control privileged operations such as declassification and delegation. (3) We sketch how the run-time principals and the acts-for hierarchy of the decentralized label model can be interpreted using public key infrastructure. \para{Acknowledgments} The authors thank Steve Chong, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich and anonymous referees for their helpful suggestions and comments on earlier drafts of this work. \bibliographystyle{ieee} \bibliography{all} \appendix \newcommand{\proofspace}{\bigskip} \section{Syntax} A secure type consists of a base type and a label. A function type $\Tfpc\Pc\Tt\Tt $ is annotated with authority $\Pc$ as a program counter that keeps track of a privileged operations $\Eo$ (such as declassify and delegate) granted by principal $\Lp$. $\Tpx$ is a singleton type for a dynamic principal $\Lp$. A capability $\Eqx$ of type $\Tc$ represents a digitally signed certificate of a principal name $\Lx$ granting a privileged operation $\Eo$. \[\begin{array}{rcll} \Tt & ::= & \Tuly & \mbox{Secure types} \\ \Tu & ::= && \mbox{Base types} \\ && \Tunit & \quad\mbox{unit} \\ && \Tsum\Tt\Tt & \quad\mbox{sum} \\ && \Tfpc\Pc\Tt\Tt & \quad\mbox{function} \\ && \Tpx & \quad\mbox{principal} \\ && \Tc & \quad\mbox{capability} \\ && \Tallxp\Tt & \quad\mbox{universal} \\ \\ \Vt & ::= && \mbox{Values} \\ && \Eunit & \quad\mbox{unit} \\ && \Einl\Tt\Vt & \quad\mbox{left injection}\\ && \Einr\Tt\Vt & \quad\mbox{right injection}\\ && \Efunx\Tt\Et & \quad\mbox{function}\\ && \Epx & \quad\mbox{principal constant}\\ && \Eqx & \quad\mbox{capability}\\ && \Eallx\Lp\Et & \quad\mbox{polymorphism}\\ \\ \Et & ::= && \mbox{Terms} \\ && \Vt & \quad\mbox{value} \\ && \Ev & \quad\mbox{variable} \\ && \Einl\Tt\Et & \quad\mbox{left injection} \\ && \Einr\Tt\Et & \quad\mbox{right injection} \\ && \Ecase\Et\Vt\Vt & \quad\mbox{sum case} \\ && \Eapp\Et\Et & \quad\mbox{application} \\ && \Eif\Et\Et\Et\Et & \quad\mbox{if delegate} \\ && \Edel\Et\Et\Et{} & \quad\mbox{let delegate} \\ && \Eifgranti\Et\Et\Et\Et & \quad\mbox{if certify} \\ && \Edcls\Et\Tt & \quad\mbox{declassify} \\ && \Egrant\Et\Eo{} & \quad\mbox{acquire} \\ && \Epapp\Et\Lp & \quad\mbox{instantiation} \end{array}\] \[\begin{array}{rcll} \Lp & ::= && \mbox{Principals} \\ && \Lv & \quad\mbox{variable} \\ && \Lx & \quad\mbox{name} \\ \\ \Ls & ::= & \Opt{\Lp,\Ls} & \mbox{Principal sets} \\ \Lc & ::= & \Opt{\Lp:\,\Ls} & \mbox{Policies} \\ \Ld & ::= & \Opt{\Lc;\,\Ld} & \mbox{Policy sets} \\ \Lt & ::= & \Lds\Ld\Ls & \mbox{Labels} \\ \\ \Penv & ::= & \Opt{\Penv,\Lp\delto\Lp} & \mbox{Principal environments} \\ \Ahi & ::= & \Opt{\Ahi,\Lx\delto\Lx} & \mbox{Acts-for hierarchies} \\ \Eenv & ::= & \Opt{\Eenv,\Ev:\Tt} & \mbox{Term environments} \\ \Pc & ::= & \Opt{\Pc,\Lp\grant\Eo} & \mbox{Authority} \\ \Ps & ::= & \Opt{\Ps,\Lv\mapsto\Lx} & \mbox{Principal substitutions} \\ \Es & ::= & \Opt{\Es,\Ev\mapsto\Vt} & \mbox{Term substitutions} \\ \\ \Eo & ::= && \mbox{Privileges} \\ && \dcls & \quad\mbox{declassify} \\ && \Cd{delegate}_{\Lp\delto\Lp} & \quad\mbox{delegate} \\ \end{array}\] \section{Static semantics} \subsection{Typing} A label is well-formed $\LabelD{\Lt}$ if $\Penv$ contains all free principal variables of the label. During function applications in T-Case and T-App, we check the precondition of the program counter is satisfied: $\proves\Pcb\delto{(\Pca|\Lt)}$. We also restrict the program counter to the integrity label of the branch condition $\Penv;\Eenv;\Pca|l$ such that privileged operations are robust. $\Penv\proves \Ttb-\Tta = \Ls$ computes the declassification requisite which is the set of principals whose authorities are needed in order to declassify. \[\begin{array}{cr} \fbox{$\Typep\Et\Tt$} & \fbox{Typing} \\ \\ \Rule{\Ev:\Tt \in \Eenv}{\Typep\Ev\Tt} & \rulelabel{T-Var} \\ \\ \Rule{\LabelD{\Lt}}{\Typep\Eunit\Tunitlx} & \rulelabel{T-Unit} \\ \\ \Rule{\Typep\Et\Tta & \LabelD{\Lt}} {\Typep{\Einl\Ttb\Et}{\Tsuml\Tta\Ttb}} & \rulelabel{T-Inl} \\ \\ \Rule{\Typep\Et\Ttb & \LabelD{\Lt}} {\Typep{\Einr\Tta\Et}{\Tsuml\Tta\Ttb}} & \rulelabel{T-Inr} \\ \\ \Rule{\Penv;\Eenv;\Pca\proves\Et:{\Tsuml\Tta\Ttb} \quad \Penv;\Eenv;\Pca|l \proves \Vta:{\Tfpcl\Pcb\Tta\Tt} \\ \D \proves\Pcb\delto{(\Pca|\Lt)} \quad\qquad \Penv;\Eenv;\Pca|l \proves \Vtb:{\Tfpcl\Pcb\Ttb\Tt}} {\Penv;\Eenv;\Pca\proves{\Ecase\Et\Vta\Vtb}:{\join\Tt\Lt}} & \rulelabel{T-Case} \\ \\ \Rule{\Penv;\Eenv,\Ev:\Tta;\Pc \proves \Et:\Ttb & \LabelD{\Lt}} {\Penv;\Eenv;\Empty \proves{\Efunx\Tta\Et}:{\Tfpcl\Pc\Tta\Ttb}} & \rulelabel{T-Fun} \\ \\ \Rule{\Penv;\Eenv;\Pca\proves \Eta:{\Tfpcl\Pcb\Tta\Ttb} & \Penv;\Eenv;\Pca\proves \Etb:\Tta & \D \proves\Pcb\delto{(\Pca|\Lt)}} {\Penv;\Eenv;\Pca\proves {\Eapp\Eta\Etb}:{\join\Ttb\Lt}} & \rulelabel{T-App} \\ \\ \Rule{\LabelD{\Lt}}{\Typep\Epx{\Tpl\Lx}} & \rulelabel{T-PName} \\ \\ \Rule{\LabelD{\Lt}}{\Typep\Eqx{\Tulx\Tc}} & \rulelabel{T-Cap} \\ \\ \Rule{ \Typep\Eta{\Tpl\Lpa} & \Typep\Etb{\Tpl\Lpb} & \PType{\Penv,\Lpa\delto\Lpb}{\Eenv}{\Etc}{\Tt} & \Typep\Etd\Tt} {\Typep{\Eif\Eta\Etb\Etc\Etd}{\join\Tt\Lt}} & \rulelabel{T-IfDel}\\ \\ \Rule{\Typep\Eta{\Tulx{(\Tp\Lpa)}} & \Typep\Etb{\Tpl\Lpb} & \PType{\Penv,\Lpa\delto\Lpb}\Eenv\Etc\Tt & \ActsforD\Lpa{\Pc(\Cd{delegate}_{\Lpa\delto\Lpb})}} {\Typep{\Edel\Eta\Etb\Etc}{\join\Tt\Lt}} & \rulelabel{T-LetDel} \\ \\ \Rule{ \Penv;\Eenv;\Pc\proves\Eta:{\Tul{\Tc}\Lt} & \Penv;\Eenv;\Pc\proves\Etb:{\Tpl\Lp} & \Penv;\Eenv;(\Pc,\Lp\grant i)|\Lt\proves\Etc:\Tt & \Penv;\Eenv;\Pc|\Lt\proves\Etd:\Tt} {\Penv;\Eenv;\Pc\proves{\Eifgranti\Eta\Etb\Etc\Etd}:{\join\Tt\Lt}} & \rulelabel{T-IfCert} \\ \\ \Rule{\Penv;\Eenv;\Pc\proves\Et:\Ttb & \Penv\proves \Ttb-\Tta = \Ls & \ActsforD\Ls{\Pc(\Cd{declassify})}} {\Penv;\Eenv;\Pc\proves{\Edcls\Et\Tta}:\Tta} & \rulelabel{T-Dcls} \\ \\ \Rule{\Typep\Et{\Tulx{(\Tp\Lp)}}} {\Typep{\Egrant\Et\Eo}{\Tulx{(\Tsum{\Tulx\Tc}\Tunitlx)}}} & \rulelabel{T-Acq} \end{array}\] \[\begin{array}{cr} \Rule{\PType{\Penv,\Lv\delto\Lp}{\Eenv}\Et\Tt & \Lv\not\in\dom\Penv & \LabelD{\Lt}} {\Typep{\Eallx\Lp\Et}{\Tallxpl\Tt}} & \rulelabel{T-All} \\ \\ \Rule{\Typep\Et{\Tallxl\Lpb\Tt} & \ActsforD\Lpa\Lpb} {\Typep{\Epapp\Et\Lpa}{\join\Tt\Lt}} & \rulelabel{T-PApp} \\ \\ \Rule{\Typep\Et\Tta & \Stypex\Tta\Ttb} {\Typep\Et\Ttb} & \rulelabel{T-Sub} \end{array}\] \subsection{Substitution} \begin{con}[Capture-avoiding substitution] When we write $\Esx{\Efun\Ev\Tt\Et}$, it is assumed that $\Ev\not\in\dom\Es$. When we write $\Psx{\Tall\Lv\Lp\Tt}$ or $\Psx{\Eall\Lv\Lp\Et}$, it is assumed that $\Lv\not\in\dom\Ps$. \end{con} We define $\Subsw\Et \defeq \Epsx\Et$. We define $\Esx\Ev=\Vt$ if $\Ev\mapsto\Vt\in\Es$, and $\Esx\Ev=\Ev$ otherwise. Similarly, we define $\Psx\Lv=\Lx$ if $\Lv\mapsto\Lx\in\Ps$, and $\Psx\Lv=\Lv$ otherwise. The $\diamond$ can be instantiated with any of these syntactic categories: $\Tt$, $\Tu$, $\Et$, $\Vt$, $\Lp$, $\Ls$, $\Lc$ and $\Ld$, $\Lt$, $\Penv$ and $\Eenv$. (It cannot be instantiated with $\Ahi$, $\Ps$ or $\Es$.) \[\begin{array}{cr} \fbox{$\Subsw\diamond=\diamond$} & \fbox{Substitution} \\ \\ (\Ps,\Lv\mapsto\Lx)(\diamond) = \Psx{\Subsy\diamond} & \mbox{Su-Delta} \\ \\ (\Es,\Ev\mapsto\Vt)(\Et) = \Esx{\Subsx\Et} & \mbox{Su-Gamma} \\ \\ \Subsw\Empty = \Empty & \mbox{Su-Empty} \\ \\ \Subsw{(\Tuly)} = \Tul{\Subsw\Tu}{\Subsw\Lt} & \mbox{Tsu-UL} \\ \\ \Subsw{(\Tsum\Tta\Ttb)} = \Tsum{\Subsw\Tta}{\Subsw\Ttb} & \mbox{Tsu-Sum} \\ \\ \Subsw{(\Tfun\Tta\Ttb)} = \Tfun{\Subsw\Tta}{\Subsw\Ttb} & \mbox{Tsu-Fun} \\ \\ \Subsw{(\Tpx)} = \Tp{\Subsw\Lp} & \mbox{Tsu-PName} \\ \\ \Subsw{(\Tc)} = \Tc & \mbox{Tsu-Cap} \\ \\ \Subsw{(\Tall\Lv\Lp\Tt)} = \Tall\Lv{\Subsw\Lp}{\Subsw\Tt} & \mbox{Tsu-All} \\ \\ \Subsw\Tunit = \Tunit & \mbox{Tsu-Unit} \\ \\ \Subsw\Eunit = \Eunit & \mbox{Esu-Unit} \\ \\ \Subsw\Ev = \Esx\Ev & \mbox{Esu-Var} \\ \\ \Subsw{(\Einlx\Et)} = \Einlx{\Subsw\Et} & \mbox{Esu-Inl} \\ \\ \Subsw{(\Einrx\Et)} = \Einrx{\Subsw\Et} & \mbox{Esu-Inr} \\ \\ \Subsw{(\Ecase\Et\Vta\Vtb)} = \Ecase{\Subsw\Et}{\Subsw\Vta}{\Subsw\Vtb} & \mbox{Esu-Case} \\ \\ \Subsw{(\Efun\Ev\Tt\Et)} = \Efun\Ev{\Subsw\Tt}{\Subsw\Et} & \mbox{Esu-Fun} \\ \\ \Subsw{(\Eapp\Eta\Etb)} = \Eapp{\Subsw\Eta}{\Subsw\Etb} & \mbox{Esu-App} \\ \\ \Subsw{(\Epx)} = \Epx & \mbox{Esu-PName} \\ \\ \Subsw{(\Eqx)} = \Eq\Lx{\Subsw\Eo} & \mbox{Esu-Cap} \end{array}\] \[\begin{array}{cr} \Subsw{(\Eif\Eta\Etb\Etc\Etd)} = \Eif{\Subsw\Eta}{\Subsw\Etb}{\Subsw\Etc}{\Subsw\Etd} & \mbox{Esu-IfDel} \\ \\ \Subsw{(\Eifgrant\Eta\Etb\Etc\Etd)} = \Eifgrant{\Subsw\Eta}{\Subsw\Etb}{\Subsw\Etc}{\Subsw\Etd} & \mbox{Esu-IfDel} \\ \\ \Subsw{(\Edel\Eta\Etb\Etc)} = \Edel{\Subsw\Eta}{\Subsw\Etb}{\Subsw\Etc} & \mbox{Esu-IfDel} \\ \\ \Subsw{(\Edcls\Et\Tt)} = \Edcls{\Subsw\Et}{\Subsw\Tt} & \mbox{Esu-IfDel} \\ \\ \Subsw{(\Egrant\Et\Eo)} = \Egrant{\Subsw\Et}{\Subsw\Eo} & \mbox{Esu-IfDel} \\ \\ \Subsw{(\Eall\Lv\Lp\Et)} = \Eall\Lv{\Subsw\Lp}{\Subsw\Et} & \mbox{Esu-All} \\ \\ \Subsw{(\Epapp\Eta\Lp)} = \Epapp{\Subsw\Eta}{\Subsw\Lp} & \mbox{Esu-PApp} \\ \\ \Subsw\Lv = \Psx\Lv & \mbox{Lsu-Var} \\ \\ \Subsw\Lx = \Lx & \mbox{Lsu-Name} \\ \\ \Subsw{(\Lp,\Ls)} = \Subsw\Lp,\Subsw\Ls & \mbox{Lsu-PSet} \\ \\ \Subsw{(\Lp:\;\Ls)} = \Subsw\Lp:\;\Subsw\Ls & \mbox{Lsu-Policy} \\ \\ \Subsw{(\Lc;\;\Ld)} = \Subsw\Lc;\;\Subsw\Ld & \mbox{Lsu-CSet} \\ \\ \Subsw{\Lds\Ld\Ls} = \Lds{\Subsw\Ld}{\Subsw\Ls} & \mbox{Lsu-Label} \\ \\ \Subsw{(\Penv,\Lpa\delto\Lpb)} = {\Subsw\Penv},{\Subsw\Lpa}\delto{\Subsw\Lpb} & \mbox{Su-PEnv} \\ \\ \Subsw{(\Eenv,\Ev:\Tt)} = {\Subsw\Eenv},\Ev:{\Subsw\Tt} & \mbox{Su-EEnv} \\ \\ \Subsw{(\Pc,\Lp:\Eo)} = {\Subsw\Pc},{\Subsw\Lp}:{\Subsw\Eo} & \mbox{Su-EEnv} \\ \\ \Subsw\dcls = \dcls & \mbox{Su-Dcls} \\ \\ \Subsw{(\del_{\Lpa\delto\Lpb})} = \del_{\Subsw\Lpa\delto\Subsw\Lpb} & \mbox{Su-Del} \end{array}\] \subsection{Subtyping} Note that we disallow subtyping with singleton principal--allowing it will break type soundness and noninterference. \[\begin{array}{cr} \fbox{$\ActsforD{p}{p}$} & \fbox{Acts-for} \\ \\ \ActsforD\Lp\Lp & \mbox{A-Refl} \\ \\ \Rule{\ActsforD\Lpa\Lpb & \ActsforD\Lpb\Lpc} {\ActsforD\Lpa\Lpc} & \mbox{A-Trans} \\ \\ \ActsforD\Lp\Ltop & \mbox{A-Top} \\ \\ \Rule{\Lpa\delto\Lpb\in\Penv} {\ActsforD\Lpa\Lpb} & \mbox{A-Constr} \\ \\ \Rule{fv(l) \subseteq \dom{\Penv}} {\LabelD{l}} & \fbox{Ok-Label} \\ \\ {\join\Tuly\Ltp = \Tul\Tu{\join\Lt\Ltp}} & \fbox{J-UL} \end{array}\] \[\begin{array}{cr} \Rule{\Stypex\Tu\Tup & \LleqD\Lt\Ltp} {\Stypex\Tuly{\Tul\Tup\Ltp}} & \fbox{St-UL} \\ \\ \fbox{$\Stypex\Tu\Tu$} & \fbox{Base Subtyping} \\ \\ \Stypex\Tu\Tu & \mbox{St-Refl} \\ \\ \Rule{\Stypex\Tu\Tup & \Stypex\Tup\Tupp} {\Stypex\Tu\Tupp} & \mbox{St-Trans} \\ \\ \Rule{\Stypex\Tta\Ttap & \Stypex\Ttb\Ttbp} {\Stypex{(\Tsum\Tta\Ttb)}{(\Tsum\Ttap\Ttbp)}} & \mbox{St-Sum} \\ \\ \Rule{\Stypex\Ttap\Tta & \Stypex\Ttb\Ttbp} {\Stypex{(\Tfun\Tta\Ttb)}{(\Tfun\Ttap\Ttbp)}} & \mbox{St-Fun} \\ \\ \Rule{\ActsforD\Lpp\Lp & \Stype{\Penv,\Lv\delto\Lpp}\Tt\Ttp} {\Stypex{(\Tallx\Lp\Tt)}{(\Tallx\Lpp\Ttp)}} & \mbox{St-All} \end{array}\] \subsection{Declassification and models} $\Penv\proves \Ttb-\Tta = \Ls$ computes the declassification requisite which is the set of principals whose authorities are needed in order to declassify. The notation \Pmodx\ denotes a substitution \Ps\ that assigns each free principal variable \Lv\ in hierarchy \Penv\ to a principal name \Lx. Similarly, $\Emodz{\Psx\Eenv}$ denotes a term substitution \Es\ that assigns each free term variable \Ev\ in environment \Eenv\ to a value such that the assignment respects the typing $\Ev:\Tt$ in \Eenv. \[\begin{array}{cr} \fbox{$\Penv\proves\Tt-\Tt=\Ls$} & \fbox{Declassification requisite} \\ \\ \Rule{\Penv\proves\Tu-\Tup=\Lsa & \Penv\proves\Lt-\Ltp=\Lsb} {\Penv\proves\Tul\Tu\Lt-\Tul\Tup\Ltp=\Lsa\cup\Lsb} & \rulelabel{D-UL} \\ \\ \Penv\proves\Tunit-\Tunit=\Empty & \mbox{D-Unit} \\ \\ \Rule{\Penv\proves\Tta-\Ttap=\Lsa & \Penv\proves\Ttb-\Ttbp=\Lsb} {\Penv\proves(\Tsum\Tta\Ttb)-(\Tsum\Ttap\Ttbp)=\Lsa\cup\Lsb} & \rulelabel{D-Sum} \\ \\ \Rule{\Penv\proves\Ttap-\Tta=\Lsa & \Penv\proves\Ttb-\Ttbp=\Lsb} {\Penv\proves(\Tfun\Tta\Ttb)-(\Tfun\Ttap\Ttbp)=\Lsa\cup\Lsb} & \rulelabel{D-Fun} \\ \\ \Penv\proves\Tpx-\Tpx=\Empty & \mbox{D-PName} \\ \\ \Rule{\Penv,\Lv\delto\Lp\proves\Tt-\Ttp=\Ls} {\Penv\proves(\Tallxp\Tt)-(\Tallxp\Ttp)=\Ls} & \rulelabel{D-All} \\ \\ \Rule{s' = \{p \sep \Penv\proves d_2(p)\delto d_1(p),\; \Penv\proves d_1(p)\not\delto d_2(p)\}} {\Penv\proves\lbl{d_1}\Ls-\lbl{d_2}\Ls=s'} & \rulelabel{D-Label} \end{array}\] \[\begin{array}{cr} \fbox{$\Emodx$} & \fbox{ESubs model} \\ \\ \Emod\Empty\Empty & \mbox{Em-Nil} \\ \\ \Rule{\Emody\Eenv & \Typep\Vt\Tt} {\Emod{\Es,\Ev\mapsto\Vt}{\Eenv,\Ev:\Tt}} & \mbox{Em-Cons} \\ \\ \fbox{$\Pmodx$} & \fbox{PSubs model} \\ \\ \Mod\Empty\Empty & \mbox{Pm-Nil} \\ \\ \Rule{\Mod\Ps\Penv & \Penv\proves\Lpa\delto\Lpb} {\Mod{\Ps,\Lv\mapsto\Lpa}{\Penv,\Lv\delto\Lpb}} & \mbox{Pm-Var} \\ \\ \Rule{\Mod\Ps\Penv} {\Mod\Ps{\Penv,\Lx\delto\Lpb}} & \mbox{Pm-Name} \\ \\ \Rule{fv(\Eenv) \subseteq \dom\Penv} {\Penv\proves\Eenv} & \fbox{EEnv Ok} \end{array}\] \section{Dynamic semantics} At run-time, E-IfDelYes checks if delegation from \Lxa\ to \Lxb\ is satisfiable in the acts-for hierarchy \Ahi. E-LetDel adds delegation to the hierarchy. E-IfCertYes cryptographically verifies if a certificate is valid. E-AcqYes enquires the external environment \E\ if a principal \Lp\ is granting the privileged operation \Eo. \[\begin{array}{cr} \fbox{$\Evalx\Et\Et$} & \fbox{Evaluation} \\ \\ \Rule{\Evalx\Et\Etp}{\Evalx{\Einl\Tt\Et}{\Einl\Tt\Etp}} & \rulelabel{E-Inl} \\ \\ \Rule{\Evalx\Et\Etp}{\Evalx{\Einr\Tt\Et}{\Einr\Tt\Etp}} & \rulelabel{E-Inr} \\ \\ \Rule{\Evalx\Et\Etp} {\Evalx{\Ecase\Et\Vta\Vtb}{\Ecase\Etp\Vta\Vtb}} & \rulelabel{E-Case} \\ \\ \Evalx{\Ecase{(\Einl\Tt\Vt)}\Vta\Vtb}{\Eapp\Vta\Vt} & \mbox{E-CaseInl} \\ \\ \Evalx{\Ecase{(\Einr\Tt\Vt)}\Vta\Vtb}{\Eapp\Vtb\Vt} & \mbox{E-CaseInr} \\ \\ \Rule{\Evalx\Eta\Etap}{\Evalx{\Eapp\Eta\Etb}{\Eapp\Etap\Etb}} & \rulelabel{E-App1} \\ \\ \Rule{\Evalx\Et\Etp}{\Evalx{\Eapp\Vt\Et}{\Eapp\Vt\Etp}} & \rulelabel{E-App2} \\ \\ \Evalx{\Eapp{(\Efunx\Tt\Et)}\Vt}{\Subsx\Et} & \mbox{E-AppFun} \\ \\ \Rule{\Evalx\Eta\Etap} {\Evalx{\Eif\Eta\Etb\Etc\Etd}{\Eif\Etap\Etb\Etc\Etd}} & \rulelabel{E-IfDel1} \\ \\ \Rule{\Evalx\Etb\Etbp} {\Evalx{\Eif\Vt\Etb\Etc\Etd}{\Eif\Vt\Etbp\Etc\Etd}} & \rulelabel{E-IfDel2} \\ \\ \Rule{\Actsfora\Lxa\Lxb} {\Evalx{\Eif{\Ep\Lxa}{\Ep\Lxb}\Etc\Etd}\Etc} & \rulelabel{E-IfDelYes} \\ \\ \Rule{\NotActsfora\Lxa\Lxb} {\Evalx{\Eif{\Ep\Lxa}{\Ep\Lxb}\Etc\Etd}\Etd} & \rulelabel{E-IfDelNo} \end{array}\] \[\begin{array}{cr} \Rule{\Evalx\Etb\Etbp} {\Evalx{\Edel\Vt\Etb\Etc}{\Edel\Vt\Etbp\Etc}} & \rulelabel{E-LetDel1} \\ \\ \Rule{\Evalx\Eta\Etap} {\Evalx{\Edel\Eta\Etb\Etc}{\Edel\Etap\Etb\Etc}} & \rulelabel{E-LetDel2} \\ \\ \Rule{(\Ahi,\Lxa\delto\Lxb),\Etc\eval(\Ahi,\Lxa\delto\Lxb),\Etcp} {\Evalx{\Edel{\Ep\Lxa}{\Ep\Lxb}\Etc}{\Edel{\Ep\Lxa}{\Ep\Lxb}\Etcp}} & \rulelabel{E-LetDel} \\ \\ \Evalx{\Edel{\Ep\Lxa}{\Ep\Lxb}\Vt}\Vt & \rulelabel{E-LetDelV} \\ \\ \Rule{\Evalx\Eta\Etap} {\Evalx{\Eifgranti\Eta\Etb\Etc\Etd}{\Eifgranti\Etap\Etb\Etc\Etd}} & \rulelabel{E-IfCert1} \\ \\ \Rule{\Evalx\Etb\Etbp} {\Evalx{\Eifgranti\Vt\Etb\Etc\Etd}{\Eifgranti\Vt\Etbp\Etc\Etd}} & \rulelabel{E-IfCert2} \\ \\ \Rule{\Ahi\proves{\Eq\Lxa\Eo}\certify{\Ep\Lxb}\grant\Eo} {\Evalx{\Eifgranti{\Eq\Lxa\Eo}{\Ep\Lxb}\Etc\Etd}\Etc} & \rulelabel{E-IfCertYes} \\ \\ \Rule{\Ahi\proves{\Eq\Lxa\Eo}\not\certify{\Ep\Lxb}\grant\Eo} {\Evalx{\Eifgranti{\Eq\Lxa\Eo}{\Ep\Lxb}\Etc\Etd}\Etd} & \rulelabel{E-IfCertNo} \\ \\ \Rule{\Evalx\Et\Etp} {\Evalx{\Edcls\Et\Tt}\Etp} & \mbox{E-Dcls1} \\ \\ \Evalx{\Edcls\Vt\Tt}\Vt & \mbox{E-Dcls2} \\ \\ \Rule{\Evalx\Et\Etp} {\Evalx{\Egrant\Et\Eo}{\Egrant\Etp\Eo}} & \rulelabel{E-Acq} \\ \\ \Rule{\E\proves{\Eq\Lx\Eo}} {\Evalx{\Egrant{\Ep\Lx}\Eo}{\Einl\Tt{\Eq\Lx\Eo}}} & \rulelabel{E-AcqYes} \\ \\ \Rule{\E\not\proves{\Eq\Lx\Eo}} {\Evalx{\Egrant{\Ep\Lx}\Eo}{\Einr\Tt\Eunit}} & \rulelabel{E-AcqNo} \\ \\ \Rule{\Evalx\Et\Etp}{\Evalx{\Epapp\Et\Lx}{\Epapp\Etp\Lx}} & \rulelabel{E-PApp} \\ \\ \Evalx{\Epapp{(\Eallxp\Et)}\Lx}{\Subs\Lv\Lx\Et} & \mbox{E-PAppAll} \end{array}\] \[\begin{array}{cr} \fbox{$\Evalmx\Et\Et$} & \fbox{Multistep eval}\\ \\ \Evalmx\Vt\Vt & \mbox{EM-Refl} \\ \\ \Rule{\Evalx\Et\Etp & \Evalmx\Etp\Etpp} {\Evalmx\Et\Etpp} & \mbox{EM-Trans} \\ \end{array}\] \section{Theorems} This section proves the soundness of the language with respect to the operational semantics: progress and preservation theorems. The main lemma is substitution for typing and subtyping. Canonical forms, inversion and weakening are standard for languages with subtyping. \begin{lem}[Canonical forms]\label{lem:canonical}\ \begin{enumerate} \item If $\Typeb\Vt{\Tsuml\Tta\Ttb}$, then $\Vt=\Einl\Ttb\Vta$ or $\Vt=\Einr\Tta\Vtb$ \item If $\Typeb\Vt{\Tfpcl\Pcb\Tta\Ttb}$, then $\Vt=\Efunx\Tt\Et$. \item If $\Typeb\Vt{\Tpl\Lx}$, then $\Vt=\Ep\Lx$. \item If $\Typeb\Vt{\Tulx\Tc}$, then $\Vt=\Eqx$. \item If $\Typeb\Vt{\Talll\Lv\Lp\Tt}$, then $\Vt=\Eallx\Lpp\Et$. \item If $\Typeb{\Epapp\Vt\Lp}\Tt$, then $\Lp=\Lx$. \end{enumerate} \end{lem} \begin{thm}[Progress] If $\Typeb\Et\Tt$, then $\Et=\Vt$ or $\Evalx\Et\Etp$. \end{thm} \begin{proof} By induction on typing derivations: \begin{itemize}\proofspace \item T-Var: $\Rule{\Ev:\Tt \in \Empty}{\Typeb\Ev\Tt}$ But $\Empty$ cannot contain $\Ev:\Tt$, and hence this case does not apply. \item T-Unit: $\Rule{\LabelZ{\Lt}}{\Typeb\Eunit\Tunitlx}$ $\Et$ is a value. \item T-Inl: $\Rule{\Typeb\Eta\Tta & \LabelZ{\Lt}} {\Typeb{\Einl\Ttb\Eta}{\Tsuml\Tta\Ttb}}$ By IH on $\Eta$, \begin{enumerate} \item $\Eta=\Vt$: $\Et=\Einl\Ttb\Vt$ is a value. \item $\Evalx\Eta\Etap$: by E-Inl, $\Etp=\Einl\Ttb\Etap$. \end{enumerate} \item T-Inr: symmetric to T-Inl. \item T-Case: $\Rule{\Typeb\Etz{\Tsuml\Tta\Ttb} & \Typeb\Vta{\Tfpcl\Pcb\Tta\Ttz} & \Typeb\Vtb{\Tfpcl\Pcb\Ttb\Ttz} & \Ahi \proves\Pcb\delto{(\Pc|\Lt)}} {\Typeb{\Ecase\Etz\Vta\Vtb}{\join\Ttz\Lt}}$ By IH on $\Etz$, \begin{enumerate} \item $\Evalx\Etz\Etzp$: by E-Case, $\Etp=\Ecase\Etzp\Vta\Vtb$. \item $\Etz=\Vt$: by Lemma~\ref{lem:canonical} (canonical forms), \begin{enumerate} \item $\Etz=\Einl\Ttb\Vtz$: by E-CaseInl, $\Etp=\Eapp\Vta\Vtz$. \item $\Etz=\Einr\Tta\Vtz$: by E-CaseInr, $\Etp=\Eapp\Vtb\Vtz$. \end{enumerate} \end{enumerate} \item T-Fun: $\Rule{\Ahi;{\Ev:\Tta};\proves\Etz:\Ttb & \Ev\not\in\dom\Empty & \LabelZ{\Lt}} {\Typeb{\Efunx\Tta\Etz}{\Tfpc\Empty\Tta\Ttb}}$ $\Et$ is a value. \item T-App: $ \Rule{\Typeb \Eta{\Tfpcl\Pcb\Tta\Ttb} & \Typeb\Etb\Tta & \Ahi \proves\Pcb\delto{(\Pc|\Lt)}} {\Typeb {\Eapp\Eta\Etb}{\join\Ttb\Lt}}$ By IH on $\Eta$ and $\Etb$, \begin{enumerate} \item $\Evalx\Eta\Etap$: by E-App1, $\Etp=\Eapp\Etap\Etb$. \item $\Eta=\Vt$ and $\Evalx\Etb\Etbp$: by E-App2, $\Etp=\Eapp\Vt\Etbp$. \item $\Eta=\Vta$ and $\Etb=\Vtb$: by Lemma~\ref{lem:canonical} (canonical forms), $\Eta=\Efunx\Tt'\Etz$ and then by E-AppFun, $\Etp=\Subs\Ev\Vtb\Etz$. \end{enumerate} \item T-PName: $\Rule{\LabelZ{\Lt}}{\Typeb\Epx{\Tpl\Lx}}$ $\Et$ is a value. \item T-Cap: $\Rule{\LabelZ{\Lt}}{\Typeb\Eqx{\Tulx\Tc}}$ $\Et$ is a value. \item T-IfDel: $\Rule{ \Typeb\Eta{\Tpl\Lpa} & \Typeb\Etb{\Tpl\Lpb} & \Ahi,\Lpa\delto\Lpb;;\Pc\proves\Etc:\Ttz & \Typeb\Etd\Ttz} {\Typeb{\Eif\Eta\Etb\Etc\Etd}{\join\Ttz\Lt}}$ By IH on $\Eta$ and $\Etb$, \begin{enumerate} \item $\Evalx\Eta\Etap$: by E-IfDel1, $\Etp=\Eif\Etap\Etb\Etc\Etd$. \item $\Eta=\Vt$ and $\Evalx\Etb\Etbp$: by E-IfDel2, $\Etp=\Eif\Vt\Etbp\Etc\Etd$. \item $\Eta=\Vta$ and $\Etb=\Vtb$: by Lemma~\ref{lem:canonical} (canonical forms), \begin{enumerate} \item $\Eta=\Ep\Lxa$, $\Etb=\Ep\Lxb$ and $\Ahi\proves\Lxa\delto\Lxb$: by E-IfDelYes, $\Etp=\Etc$. \item $\Eta=\Ep\Lxa$, $\Etb=\Ep\Lxb$ and $\Ahi\proves\Lxa\not\delto\Lxb$: by E-IfDelNo, $\Etp=\Etd$. \end{enumerate} \end{enumerate} \item T-LetDel: $\Rule{ \Typeb\Eta{\Tpl\Lpa} & \Typeb\Etb{\Tpl\Lpb} & \Ahi,\Lpa\delto\Lpb;;\Pc\proves \Etc:\Ttz & \Actsfora\Lpa{\Pc(\Cd{delegate}_{\Lpa\delto\Lpb})}} {\Typeb{\Edel\Eta\Etb\Etc}{\join\Ttz\Lt}}$ By IH on $\Eta$ and $\Etb$, \begin{enumerate} \item $\Evalx\Eta\Etap$: by E-LetDel1, $\Etp=\Edel\Etap\Etb\Etc$. \item $\Eta=\Vt$ and $\Evalx\Etb\Etbp$: by E-LetDel2, $\Etp=\Edel\Vt\Etbp\Etc$. \item $\Eta=\Vta$ and $\Etb=\Vtb$: by Lemma~\ref{lem:canonical} (canonical forms), $\Eta=\Ep\Lxa$ and $\Etb=\Ep\Lxb$. Then, by IH on $\Etc$, we have $\Etp={\Edel{\Ep\Lxa}{\Ep\Lxb}\Etcp}$ (by E-LetDel), or we have $\Etp=\Vt$ (by E-LetDelV). \end{enumerate} \item T-IfCert: $\Rule{ \Ahi\proves\Eta:{\Tul{\Tc}\Lt} & \Ahi\proves\Etb:{\Tpl\Lp} & \Ahi;;(\Pc,\Lp\grant i)|\Lt\proves\Etc:\Ttz & \Ahi;;\Pc|\Lt\proves\Etd:\Ttz} {\Ahi\proves{\Eifgranti\Eta\Etb\Etc\Etd}:{\join\Ttz\Lt}}$ By IH on $\Eta$ and $\Etb$, \begin{enumerate} \item $\Evalx\Eta\Etap$: by E-IfCert1, $\Etp=\Eifgranti\Etap\Etb\Etc\Etd$. \item $\Eta=\Vt$ and $\Evalx\Etb\Etbp$: by E-IfCert2, $\Etp=\Eifgranti\Vt\Etbp\Etc\Etd$. \item $\Eta=\Vta$ and $\Etb=\Vtb$: by Lemma~\ref{lem:canonical} (canonical forms), \begin{enumerate} \item $\Eta=\Eqx$, $\Etb=\Ep\Lx$ and $\Ahi\proves{\Eq\Lxa\Eo}\certify{\Ep\Lxb}\grant\Eo$: by E-IfCertYes, $\Etp=\Etc$. \item $\Eta=\Ep\Lx$, $\Etb=\Ep\Lx$ and $\Ahi\proves{\Eq\Lxa\Eo}\not\certify{\Ep\Lxb}\grant\Eo$: by E-IfCertNo, $\Etp=\Etd$. \end{enumerate} \end{enumerate} \item T-Dcls: $\Rule{\Ahi\proves\Etz:\Ttb & \Ahi\proves \Ttb-\Tta = \Ls & \Actsfora\Ls{\Pc(\Cd{declassify})}} {\Ahi\proves{\Edcls\Etz\Tta}:\Tta}$ By E-Dcls1 or E-Dcls2. \item T-Acq: $\Rule{\Typeb\Etz{\Tulx{(\Tp\Lp)}}} {\Typeb{\Egrant\Etz\Eo}{\Tulx{(\Tsum{\Tulx\Tc}\Tunitlx)}}}$ By IH on $\Etz$, \begin{enumerate} \item $\Evalx\Etz\Etzp$: by E-Acq, $\Etp=\Egrant\Etzp\Eo$. \item $\Etz=\Vt$: by Lemma~\ref{lem:canonical} (canonical forms), $\Etz=\Eqx$. Then, either \begin{enumerate} \item $\E\proves{\Eq\Lx\Eo}$: by E-AcqYes, $\Etp=\Einl\Ttz{\Eq\Lx\Eo}$. \item $\E\not\proves{\Eq\Lx\Eo}$: by E-AcqNo, $\Etp=\Einr\Ttz\Eunit$. \end{enumerate} \end{enumerate} \item T-All: $\Rule{\Ahi,\Lv\delto\Lp\proves\Etz:\Ttz & \Lv\not\in\dom\Ahi & \LabelZ{\Lt}} {\Typeb{\Eallxp\Etz}{\Tallxpl\Ttz}}$ $\Et$ is a value. \item T-PApp: $\Rule{\Typeb\Etz{\Tallxpl\Ttz}} {\Typeb{\Epapp\Etz\Lp}{\join\Ttz\Lt}}$ By IH on $\Etz$, \begin{enumerate} \item $\Evalx\Etz\Etzp$: by E-PApp, $\Etp=\Epapp\Etzp\Lp$. \item $\Etz=\Vt$: by Lemma~\ref{lem:canonical} (canonical forms), $\Etz=\Eallxp\Eta$ and $\Lp=\Lx$. Then, by E-PAppAll, $\Etp=\Subs\Lv\Lx\Eta$. \end{enumerate} \item T-Sub: $\Rule{\Typeb\Etz\Tta & \Stypea\Tta\Ttb} {\Typeb\Etz\Ttb}$ By IH on $\Etz$. \end{itemize} \end{proof} \begin{lem}[Inversion]\label{lem:inversion}\ \begin{enumerate} \item If $\Typep{\Einl\Tt\Vt}{\Tsuml\Tta\Ttb}$, then $\Typep\Vt\Tta$. \item If $\Typep{\Einr\Tt\Vt}{\Tsuml\Tta\Ttb}$, then $\Typep\Vt\Ttb$. \item If $\Typep{\Efunx\Tta\Et}{\Tfunl\Tta\Ttb}$, then $\Typey\Et\Ttb$. \item If $\Typep{\Eallxp\Et}{\Tallxpl\Tt}$, then $\PType{\Penv,\Lv\delto\Lp}\Eenv\Et\Tt$. \end{enumerate} \end{lem} \begin{proof} By normalizing the typing derivations (collapsing multiple applications of T-Sub into one application of T-Sub). \end{proof} \begin{lem}[Weakening]\label{lem:weaken}\ \begin{enumerate} \item If $\Typep\Et\Tt$, then ${\Penv,\Lpa\delto\Lpb};{\Eenv,\Ev:\Ttp};{\Pc,\Lp\grant\Eo} \proves\Et:\Tt$. \item If $\Pca\delto\Pcb$ and $\Pcb\delto\Pcc$, then $\Pca\delto\Pcc$. \end{enumerate} \end{lem} \begin{lem}[Substitution for join]\label{lem:subs-join}\ $\Psx{\join\Tt\Lt} = \join{\Psx\Tt}{\Psx\Lt}$ \end{lem} \begin{lem}[Substitution for subtyping]\label{lem:subs-sub-full}\ \begin{enumerate} \item If $\Stypex\Tta\Ttb$, $\Pmodx$ and $\Ahi=\Psx\Penv$, then $\Stypea{\Psx\Tta}{\Psx\Ttb}$ \item If $\LleqD\Lta\Ltb$, $\Pmodx$ and $\Ahi=\Psx\Penv$, then $\Lleqa{\Psx\Lta}{\Psx\Ltb}$ \item If $\LleqD\Lca\Lcb$, $\Pmodx$ and $\Ahi=\Psx\Penv$, then $\Lleqa{\Psx\Lca}{\Psx\Lcb}$ \item If $\ActsforD\Lpa\Lpb$, $\Pmodx$ and $\Ahi=\Psx\Penv$, then $\Actsfora{\Psx\Lpa}{\Psx\Lpb}$ \item If $\Stype{\Penv,\Lv\delto\Lp}\Tta\Ttb$ and $\ActsforD\Lpp\Lp$, then $\Stype{\Subs\Lv\Lpp{\Penv}}{\Subs\Lv\Lpp\Tta}{\Subs\Lv\Lpp\Ttb}$. \item If $\Lleq{\Penv,\Lv\delto\Lp}\Lta\Ltb$ and $\ActsforD\Lpp\Lp$, then $\Lleq{\Subs\Lv\Lpp{\Penv}}{\Subs\Lv\Lpp\Lta}{\Subs\Lv\Lpp\Ltb}$. \item If $\Lleq{\Penv,\Lv\delto\Lp}\Lca\Lcb$ and $\ActsforD\Lpp\Lp$, then $\Lleq{\Subs\Lv\Lpp{\Penv}}{\Subs\Lv\Lpp\Lca}{\Subs\Lv\Lpp\Lcb}$. \item If $\Actsfor{\Penv,\Lv\delto\Lp}\Lpa\Lpb$ and $\ActsforD\Lpp\Lp$, then $\Actsfor{\Subs\Lv\Lpp{\Penv}}{\Subs\Lv\Lpp\Lpa}{\Subs\Lv\Lpp\Lpb}$. \end{enumerate} \end{lem} The last four rules are special cases of the first four. The first four rules are used in proving Lemma~\ref{lem:subs-logical-full} (substitution for logical relations), while the last four are used in proving Lemma~\ref{lem:subs-typing-full} (substitution for typing). Similarly, substitution also respects subtyping for base types, principal sets, and policy sets. \begin{lem}[Substitution for typing]\label{lem:subs-typing-full}\ \begin{enumerate} \item If $\Typep\Et\Tt$, $\Pmodx$, $\Ahi=\Psx\Penv$ and $\Emodz{\Psx\Eenv}$, then $\Typeb{\Epsx\Et}{\Psx\Tt}$. \item If $\Typew\Et\Tt$ and $\Typep\Vt\Ttp$, then $\Typep{\Subsx\Et}\Tt$. \item If $\PType{\Penv,\Lv\delto\Lp}\Eenv\Et\Tt$, then ${\Subs\Lv\Lx\Penv};{\Subs\Lv\Lx\Eenv};{\Subs\Lv\Lx\Pc}\proves {\Subs\Lv\Lx\Et}:{\Subs\Lv\Lx\Tt}$. \end{enumerate} \end{lem} The last two rules are special cases of the first. The first rule is used in proving Lemma~\ref{lem:subs-logical-full} (substitution for logical relations), while the last two are used in proving Theorem~\ref{thm-preser} (preservation). \newcommand{\weaken}{Lemma~\ref{lem:weaken} (weakening) } \begin{thm}[Preservation] \label{thm-preser} If $\Typeb\Et\Tt$ and $\Evalx\Et\Etp$, then $\Typec\Etp\Tt$ such that $\Ahi\delto\Ahi'$ and $\Pc\delto\Pc'$. \end{thm} \begin{proof} % (query-replace "\\Penv;\\Eenv;" "\\Ahi;" nil) % (query-replace "typep" "typeb" nil) By induction on the typing derivations: \begin{itemize}\proofspace \item T-Var: $ \Rule{\Ev:\Tt \in \Eenv}{\Typeb\Ev\Tt}$ $\Et$ has no evaluation rule, hence this case does not apply. \item T-Unit: $ \Rule{\LabelZ{\Lt}}{\Typeb\Eunit\Tunitlx}$ $\Et$ has no evaluation rule, hence this case does not apply. \item T-Inl: $\Rule{\Typeb\Eta\Tta & \LabelZ{\Lt}} {\Typeb{\Einl\Ttb\Eta}{\Tsuml\Tta\Ttb}}$ There is one possible evaluation rule, E-Inl: $\Rule{\Evalx\Eta\Etap}{\Evalx{\Einl\Ttb\Eta}{\Einl\Ttb\Etap}}$ By IH on $\Eta$, we have $\Typec\Etap\Tta$. The result follows by T-Inl. \item T-Inr: symmetric to T-Inl. \item T-Case: $ \Rule{\Ahi;;\Pc\proves\Etz:{\Tsuml\Tta\Ttb} & \Ahi;;\Pc|l \proves \Vta:{\Tfpcl\Pcb\Tta\Ttz} & \Ahi;;\Pc|l \proves \Vtb:{\Tfpcl\Pcb\Ttb\Ttz} & \Ahi \proves\Pcb\delto{(\Pc|\Lt)}} {\Ahi;;\Pc\proves{\Ecase\Etz\Vta\Vtb}:{\join\Ttz\Lt}}$ There are three possible evaluation rules: \begin{enumerate} \item E-Case: $\Rule{\Evalx\Etz\Etzp} {\Evalx{\Ecase\Etz\Vta\Vtb}{\Ecase\Etzp\Vta\Vtb}}$ By IH on $\Etz$, we have $\Typec\Etzp{\Tsuml\Tta\Ttb}$. The result follows by \weaken and T-Case. \item E-CaseInl: $\Evalx{\Ecase{(\Einl\Ttb\Vt)}\Vta\Vtb}{\Eapp\Vta\Vt}$ By Lemma~\ref{lem:inversion} (inversion), $\Typeb\Vt\Tta$. The result follows by \weaken and T-App. \item E-CaseInr: symmetric to E-CaseInl. \end{enumerate} \item T-Fun: $ \Rule{\Ahi;\Ev:\Tta;\Pc \proves \Etz:\Ttb & \LabelZ{\Lt}} {\Ahi;;\Pc \proves{\Efunx\Tta\Etz}:{\Tfpcl\Pc\Tta\Ttb}}$ $\Et$ has no evaluation rule, hence this case does not apply. \item T-App: $ \Rule{\Ahi;;\Pca\proves \Eta:{\Tfpcl\Pcb\Tta\Ttb} & \Ahi;;\Pca\proves \Etb:\Tta & \Ahi \proves\Pcb\delto{(\Pca|\Lt)}} {\Ahi;;\Pca\proves {\Eapp\Eta\Etb}:{\join\Ttb\Lt}}$ There are three possible evaluation rules: \begin{enumerate} \item E-App1: $\Rule{\Evalx\Eta\Etap}{\Evalx{\Eapp\Eta\Etb}{\Eapp\Etap\Etb}}$ By IH on $\Eta$, we have $\Typec\Etap{\Tfpcl\Pcb\Tta\Ttb}$. The result follows by \weaken and T-App. \item E-App2: similar to E-App1. \item E-AppFun: $\Evalx{\Eapp{(\Efunx\Tta\Etz)}\Vt}{\Subsx\Etz}$ By Lemma~\ref{lem:inversion} (inversion), $\Typey\Etz\Ttb$. Then, by Lemma~\ref{lem:subs-typing-full} (substitution for typing), $\Typeb{\Subsx\Etz}\Ttb$. The result follows by T-Sub. \end{enumerate} \item T-PName: $ \Rule{\LabelZ{\Lt}}{\Typeb\Epx{\Tpl\Lx}}$ $\Et$ has no evaluation rule, hence this case does not apply. \item T-Cap: $ \Rule{\LabelZ{\Lt}}{\Typeb\Eqx{\Tulx\Tc}}$ $\Et$ has no evaluation rule, hence this case does not apply. \item T-IfDel: $ \Rule{ \Typeb\Eta{\Tpl\Lpa} & \Typeb\Etb{\Tpl\Lpb} & \Ahi,\Lpa\delto\Lpb;;\Pc\proves\Etc:\Ttz & \Typeb\Etd\Ttz} {\Typeb{\Eif\Eta\Etb\Etc\Etd}{\join\Ttz\Lt}}$ There are four possible evaluation rules: \begin{enumerate} \item E-IfDel1: $\Rule{\Evalx\Eta\Etap} {\Evalx{\Eif\Eta\Etb\Etc\Etd}{\Eif\Etap\Etb\Etc\Etd}}$ By IH on $\Eta$, we have $\Typec\Etap{\Tpl\Lxa}$. The result follows by \weaken and T-IfDel. \item E-IfDel2: similar to E-IfDel1. \item E-IfDelYes: $\Rule{\Actsfora\Lxa\Lxb} {\Evalx{\Eif{\Ep\Lxa}{\Ep\Lxb}\Etc\Etd}\Etc}$ Let $A'=\Ahi,\Lpa\delto\Lpb$. The result follows by \weaken and T-Sub. \item E-IfDelNo: similar to E-IfDelYes. \end{enumerate} \item T-LetDel: $\Rule{ \Typeb\Eta{\Tpl\Lpa} & \Typeb\Etb{\Tpl\Lpb} & \Typeb\Etc\Ttz} {\Typeb{\Edel\Eta\Etb\Etc}{\join\Ttz\Lt}}$ There are four possible evaluation rules: \begin{enumerate} \item E-LetDel1: $\Rule{\Evalx\Etb\Etbp} {\Evalx{\Edel\Vt\Etb\Etc}{\Edel\Vt\Etbp\Etc}}$ By IH on $\Eta$, we have $\Typec\Etap{\Tpl\Lpa}$. The result follows by \weaken and T-LetDel. \item E-LetDel2: similar to E-LetDel1. \item E-LetDel: similar to E-LetDel1. \item E-LetDel: by \weaken and T-Sub. \end{enumerate} \item T-IfCert: $ \Rule{ \Ahi;;\Pc\proves\Eta:{\Tul{\Tc}\Lt} & \Ahi;;\Pc\proves\Etb:{\Tpl\Lp} & \Ahi;(\Pc,\Lp\grant i)|\Lt\proves\Etc:\Ttz & \Ahi;;\Pc|\Lt\proves\Etd:\Ttz} {\Ahi;;\Pc\proves{\Eifgranti\Eta\Etb\Etc\Etd}:{\join\Ttz\Lt}}$ There are four possible evaluation rules: \begin{enumerate} \item E-IfCert1: $\Rule{\Evalx\Eta\Etap} {\Evalx{\Eifgranti\Eta\Etb\Etc\Etd}{\Eifgranti\Etap\Etb\Etc\Etd}}$ By IH on $\Eta$, we have $\Typec\Etap{\Tul{\Tc}\Lt}$. The result follows by \weaken and T-IfCert. \item E-IfCert2: similar to E-IfCert1. \item E-IfCertYes: $\Rule{\Ahi\proves{\Eq\Lxa\Eo}\certify{\Ep\Lxb}\grant\Eo} {\Evalx{\Eifgranti{\Eq\Lxa\Eo}{\Ep\Lxb}\Etc\Etd}\Etc}$ Let $\Pc'=\Pc,\Lp\grant i$. The result follows by T-Sub. \item E-IfCertNo: similar to E-IfCertYes. \end{enumerate} \item T-Dcls: $ \Rule{\Ahi;;\Pc\proves\Etz:\Ttb & \Ahi\proves \Ttb-\Tta = \Ls & \Actsfora\Ls{\Pc(\Cd{declassify})}} {\Ahi;;\Pc\proves{\Edcls\Etz\Tta}:\Tta}$ There is two possible evaluation rule \begin{enumerate} \item E-Dcls1: $\Rule{\Evalx\Etzp\Etp} {\Evalx{\Edcls\Etz\Tt}\Etz}$ By IH on $\Etz$, we have $\Typec\Etzp\Ttb$. The result follows by \weaken and T-Dcls. \newcommand{\erasure}[1]{\lfloor{#1}\rfloor} \item E-Dcls: $\Evalx{\Edcls\Vt\Ttz}\Vt$. Assume we only declassify a label at the top-level type, that is $\Ahi\proves \Tt_{l'} -\Tt_l = \Ls$, where $\Ttb=\Tt_{l'}$ and $\Tta=\Tt_l$. Since we can assign any label to the top-level type of a value (according to T-Unit, T-Inl, T-Inr, T-Fun, T-PName, T-Cap and T-All), we can change the type of $\Vt$ from $\Typeb\Vt{\Tt_{l'}}$ to $\Typeb\Vt{\Tt_{l}}$. If we declassify a label inside the structure of a type (in particular, the parameter type of a function), we need to weaken the theorem such that evaluation preserves types only in the erasure semantics. That is, if $\Typeb\Et\Tt$ and $\Evalx{\erasure\Et}{\erasure\Etp}$, then $\Typeb{\erasure\Etp}\Tt$, where $\erasure\cdot$ is the type-erasure function. We omit the proof for this general case here. \end{enumerate} \item T-Acq: $ \Rule{\Typeb\Etz{\Tulx{(\Tp\Lp)}}} {\Typeb{\Egrant\Etz\Eo}{\Tulx{(\Tsum{\Tulx\Tc}\Tunitlx)}}}$ There are three possible evaluation rules: \begin{enumerate} \item E-Acq: $\Rule{\Evalx\Etz\Etzp} {\Evalx{\Egrant\Etz\Eo}{\Egrant\Etzp\Eo}}$ By IH on $\Etz$, we have $\Typec\Etzp{\Tul{\Tc}\Lt}$. The result follows by \weaken and T-Acq. \item E-AcqYes: $\Rule{\E\proves{\Eq\Lx\Eo}} {\Evalx{\Egrant{\Ep\Lx}\Eo}{\Einl\Tt{\Eq\Lx\Eo}}}$ By T-Cap and T-Inl. \item E-AcqNo: similar to E-AcqYes. \end{enumerate} \item T-All: $ \Rule{\PType{\Penv,\Lv\delto\Lp}{\Eenv}\Etz\Ttz & \Lv\not\in\dom\Penv & \LabelZ{\Lt}} {\Typeb{\Eallx\Lp\Etz}{\Tallxpl\Ttz}}$ $\Et$ has no evaluation rule, hence this case does not apply. \item T-PApp: $ \Rule{\Typeb\Etz{\Tallxl\Lpb\Ttz} & \Actsfora\Lpa\Lpb} {\Typeb{\Epapp\Etz\Lpa}{\join\Ttz\Lt}}$ There are two possible evaluation rules: \begin{enumerate} \item E-PApp: $\Rule{\Evalx\Etz\Etzp}{\Evalx{\Epapp\Etz\Lx}{\Epapp\Etzp\Lx}}$ By IH on $\Etz$, we have $\Typec\Etzp{\Tallxpl\Ttz}$. The result follows by \weaken and T-PApp. \item E-PAppAll: $\Evalx{\Epapp{(\Eallxp\Etz)}\Lx}{\Subs\Lv\Lx\Etz}$ By Lemma~\ref{lem:inversion} (inversion), $\TypeD{\Eenv,\Lv}\Etz{\join\Ttz\Lt}$. Then, by Lemma~\ref{lem:subs-typing-full} (substitution for typing), $\Typeb{\Subs\Lv\Lx\Etz}\Ttz$. The result follows by \weaken and T-Sub. \end{enumerate} \item T-Sub: $\Rule{\Typeb\Etz\Tta & \Stypea\Tta\Ttb} {\Typeb\Etz\Ttb}$ By IH on $\Etz$. \end{itemize} \end{proof} \begin{prop}[Join order]\label{prop:join} $\LleqD\Lta{\join\Lta\Ltb}$. \end{prop} \begin{prop}[Join commutativity]\label{prop:comm} $\join\Lta\Ltb = \join\Ltb\Lta$. \end{prop} \section{Noninterference} This section proves the main result of the paper: noninterference theorem. The main lemmas are substitution for logical relations and subtyping for logical relations. The intuition is that in secure programs, high-security inputs do not interfere with low-security outputs. The proof requires a notion of equivalence with respect to observers of different security labels. To reason about equivalence of higher-order functions and polymorphism, we use the standard technique of logical relations~\cite{Mit96}. However, we parameterize the relations with an upper-bound \Rell\ of the observer's security label, capturing the dependence of the terms' equivalence on the observer's label. The definitions and the theorems for this section are only for the core calculus--no authority, capability, declassification or delegation. Extending the result to the full calculus is left for future work. \[\begin{array}{cr} \Rule{ \Ahi\proves\Eenv \quad\Emodz\Eenv \quad\Emodzp\Eenv \\ \forall(\Ev:\Tt\in\Eenv).\; \Relv{\Esx\Ev}{\Esxp\Ev}\Tt} \Relgx & \fbox{R-Subs} \\ \\ \Rule{ \renewcommand{\arraystretch}{1} \begin{array}{l} \Evalmx\Et\Vt \quad\Evalmx\Etp\Vtp \\ \Typea\Et\Tt \quad\Typea\Etp\Tt \quad\Relvx\Tt \end{array}} {\Relex\Tt} & \fbox{R-Term} \\ \\ \fbox{$\Relv\Vt\Vt\Tt$} & \fbox{Related values} \\ \\ \Rule{\Ahi\proves\Lt\not\sle\Rell} {\Relvx\Tuly} & \mbox{R-Label} \\ \\ \raisebox{1.5ex}{\mbox{\Relv\Eunit\Eunit\Tunitlx}} & \mbox{R-Unit} \\ \\ \Rule{\Relvx\Tta} {\Relv{\Einlx\Vt}{\Einlx\Vtp}{\Tsuml\Tta\Ttb}} & \mbox{R-Inl} \\ \\ \Rule{\Relvx\Ttb} {\Relv{\Einrx\Vt}{\Einrx\Vtp}{\Tsuml\Tta\Ttb}} & \mbox{R-Inr} \\ \\ \Rule{ \forall(\Relvb\Tta).\; \Rele{(\Eapp\Vt\Vtb)}{(\Eapp\Vtp\Vtbp)}{\join\Ttb\Lt}\Rell} {\Relvx{\Tfunl\Tta\Ttb}} & \mbox{R-Fun} \\ \\ \raisebox{1.5ex}{\mbox{\Relv\Epx\Epx{\Tpl\Lx} }} & \mbox{R-PName} \\ \\ \Rule{\forall(\Actsfora\Lx\Lp).\; \Rele{(\Epapp\Vt\Lx)}{(\Epapp\Vtp\Lx)}{\join{\Tt\{X/\alpha\}}\Lt}\Rell} {\Relvx{\Tallxpl\Tt}} & \mbox{R-All} \\ \end{array}\] \begin{lem}[Subtyping for logical relations]\label{lem:sub-logical}\ \begin{enumerate} \item If $\Reley\Et\Etp\Tt$ and $\Stypea\Tt\Ttp$, then $\Reley\Et\Etp\Ttp$. \item If $\Relv\Vt\Vtp\Tt$ and $\Stypea\Tt\Ttp$, then $\Relv\Vt\Vtp\Ttp$. \item If $\Relv\Vt\Vtp\Tuly$ and $\Lleqa\Lt\Ltp$, then $\Relv\Vt\Vtp{\Tul\Tu\Ltp}$. \item If $\Relv\Vt\Vtp\Tuly$ and $\Stypea\Tu\Tup$, then $\Relv\Vt\Vtp{\Tul\Tup\Lt}$. \end{enumerate} \end{lem} \begin{proof} Part (1): By T-Sub, the result terms are well-typed. By IH of Part (2), their evaluated values are related. The result then follows by R-Term. Part (2): by St-UL, Part (3) and Part (4). Part (3): by Lst-trans and R-Label. Part (4): by induction on the subtyping derivations: \begin{itemize}\proofspace \item St-Refl: $\Stypea\Tu\Tu$ The result trivially follows because $\Tu=\Tup$. \item St-Trans: $\Rule{\Stypea\Tu\Tup & \Stypea\Tup\Tupp} {\Stypea\Tu\Tupp}$ The result follows by IH. \item St-Sum: $\Rule{\Stypea\Tta\Ttap & \Stypea\Ttb\Ttbp} {\Stypea{(\Tsum\Tta\Ttb)}{(\Tsum\Ttap\Ttbp)}}$ By the inversion of R-Sum with $\Relv\Vt\Vtp{\Tsuml\Tta\Ttb}$, either \begin{enumerate} \item R-Label with $\Ahi\proves\Lt\not\sle\Rell$: the result follows by R-Label. \item R-Inl with $\Vt=\Einlx\Vtz$, $\Vtp=\Einlx\Vtzp$ and $\Relv\Vtz\Vtzp\Tta$: by IH of Part (2) with $\Stypea\Tta\Ttap$, we have $\Relv\Vtz\Vtzp\Ttap$. The result follows by R-Inl. \item R-Inr: symmetric to the previous case. \end{enumerate} \item St-Fun: $\Rule{\Stypea\Ttap\Tta & \Stypea\Ttb\Ttbp} {\Stypea{(\Tfun\Tta\Ttb)}{(\Tfun\Ttap\Ttbp)}}$ By R-Fun, we need to show that $\forall\Relvb\Ttap$, \[ \Rele{(\Eapp\Vt\Vtb)}{(\Eapp\Vtp\Vtbp)}{\join\Ttbp\Lt}\Rell \] By IH of Part (2) with $\Stypea\Ttap\Tta$, we have $\Relv\Vtb\Vtbp\Tta$. By the inversion of R-Fun with $\Relv\Vt\Vtp{\Tfunl\Tta\Ttb}$, we have $\Rele{(\Eapp\Vt\Vtb)}{(\Eapp\Vtp\Vtbp)}{\join\Ttb\Lt}\Rell$. By St-UL with $\Stypea\Ttb\Ttbp$ and $\Lleqa\Lt\Lt$, we have $\Stypea{\join\Ttb\Lt}{\join\Ttbp\Lt}$. Then, the results follows by IH of Part (1). \item St-All: $\Rule{\Actsfora\Lpp\Lp & \Stype{\Penv,\Lv\delto\Lpp}\Ttz\Ttzp} {\Stypea{(\Tallx\Lp\Ttz)}{(\Tallx\Lpp\Ttzp)}}$ By R-All, we need to show that $\forall\Actsfora\Lx\Lpp$, \[ \Rele{(\Epapp\Vt\Lx)}{(\Epapp\Vtp\Lx)}{\join\Ttzp\Lt}\Rell \] By the inversion of R-All with $\Relv\Vt\Vtp{\Tallxl\Lp\Ttz}$, we have $\Rele{(\Epapp\Vt\Lx)}{(\Epapp\Vtp\Lx)}{\join\Ttz\Lt}\Rell$. By St-UL with $\Stypea\Ttz\Ttzp$ and $\Lleqa\Lt\Lt$, we have $\Stypea{\join\Ttz\Lt}{\join\Ttzp\Lt}$. By IH of Part (2), we have $\Relv\Vt\Vtp{\Tallxl\Lp\Ttzp}$. By J-UL and St-All with $\Stypea\Lpp\Lp$, we have $\Stypea{\Tallxl\Lp\Ttzp}{\Tallxl\Lpp\Ttzp}$. Then, the results follows by IH of Part (1). \end{itemize} \end{proof} \begin{lem}[Substitution for logical relations]\label{lem:subs-logical-full}\ If $\Typex\Et\Tt$, $\Pmodx$, $\Ahi=\Psx\Penv$ and $\Relg\Es\Esp\Rell{\Psx\Eenv}$, then \[\Reley{\Epsx\Et}{\Epsxp\Et}{\Psx\Tt}\] \end{lem} \begin{proof} Let us name the assumptions: \begin{enumerate} \item $\Typex\Et\Tt$ (Z-Type) \item $\Pmodx$ (Z-DModel) \item $\Ahi=\Psx\Penv$ (Z-IfDel) \item $\Relg\Es\Esp\Rell{\Psx\Eenv}$ (Z-RSubs) \end{enumerate} By Lemma~\ref{lem:subs-typing-full} (Part 1), the whole terms are well-typed. It remains to show that $\Evalmx{\Epsx\Et}\Vt$ and $\Evalmx{\Epsxp\Etp}\Vtp$ and \[ \Relvx\Tt \] which we prove by induction on the typing derivations. \begin{itemize}\proofspace \item T-Var: $\Rule{\Ev:\Tt\in\Eenv}{\Typex\Ev\Tt}$ The result follows by Z-RSubs and R-Subs. \item T-Unit: $\Rule{\LabelD{\Lt}}{\Typex\Eunit\Tunitlx}$ By Esu-Unit, $\Epsx\Et=\Epsxp\Et=\Eunit$. Their evaluated values are related by EM-Refl and R-Unit. The result then follows by R-Term. \item T-Inl: \setcounter{equation}0 $\Rule{\Typex\Eta\Tta & \LabelD{\Lt}} {\Typex{\Einl\Ttb\Eta}{\Tsuml\Tta\Ttb}}$ By Esu-Inl, Tsu-Inl and Lemma~\ref{lem:subs-join} (substitution for join), \begin{eqnarray} \Epsx{\Einl\Tta\Eta} &=& \Einl{\Psx\Tta}{\Epsx\Eta} \\ \Epsxp{\Einl\Tta\Eta} &=& \Einl{\Psx\Tta}{\Epsxp\Eta} \\ \Psx{\Tsuml\Tta\Ttb} &=& \Tul{(\Tsum{\Psx\Tta}{\Psx\Ttb})}{\Psx\Lt} \end{eqnarray} By IH on $\Eta$, we have $\Reley{\Epsx\Eta}{\Epsxp\Eta}{\Psx\Tta}$ with $\Evalmx{\Epsx\Eta}\Vt$ and $\Evalmx{\Epsxp\Eta}\Vtp$. By EM-Trans and E-Inl, we have $\Evalmx{\Einlx{\Epsx\Eta}}{\Einlx\Vt}$ and $\Evalmx{\Einlx{\Epsxp\Eta}}{\Einlx\Vtp}$. The result follows by (1)-(3), R-Inl and R-Term. \item T-Inr: symmetric to T-Inl. \item T-Case: $\Rule{\Typex\Etz{\Tsuml\Tta\Ttb} & \Typex\Vta{\Tfunl\Tta\Ttz} & \Typex\Vtb{\Tfunl\Ttb\Ttz}} {\Typex{\Ecase\Etz\Vta\Vtb}{\join\Ttz\Lt}}$ By IH on $\Etz$, $\Vta$ and $\Vtb$, \begin{enumerate} \item $\Reley{\Epsx\Etz}{\Epsxp\Etz}{\Psx{\Tsuml\Tta\Ttb}}$ with $\Evalmx{\Epsx\Etz}\Vtz$ and $\Evalmx{\Epsxp\Etz}\Vtzp$ \item $\Reley{\Epsx\Vta}{\Epsxp\Vta}{\Psx{\Tfunl\Tta\Ttz}}$ with $\Evalmx{\Epsx\Vta}{\Epsx\Vta}$ and $\Evalmx{\Epsxp\Vta}{\Epsxp\Vta}$ \item $\Reley{\Epsx\Vtb}{\Epsxp\Vtb}{\Psx{\Tfunl\Ttb\Ttz}}$ with $\Evalmx{\Epsx\Vtb}{\Epsx\Vtb}$ and $\Evalmx{\Epsxp\Vtb}{\Epsxp\Vtb}$ \end{enumerate} By Esu-Case and EM-Trans with E-Case, \begin{eqnarray*} \Epsx{\Ecase\Etz\Vta\Vtb} &=& \Ecase{\Epsx\Etz}{\Epsx\Vta}{\Epsx\Vtb} \\ \Epsxp{\Ecase\Etz\Vta\Vtb} &=& \Ecase{\Epsxp\Etz}{\Epsxp\Vta}{\Epsxp\Vtb} \\ \Ahi,{\Ecase{\Epsx\Etz}{\Epsx\Vta}{\Epsx\Vtb}} &\evalm& \Ahi,{\Ecase\Vtz{\Epsx\Vta}{\Epsx\Vtb}} \\ \Ahi,{\Ecase{\Epsxp\Etz}{\Epsxp\Vta}{\Epsxp\Vtb}} &\evalm& \Ahi,{\Ecase\Vtzp{\Epsxp\Vta}{\Epsxp\Vtb}} \end{eqnarray*} By Tsu-Sum and the inversion of $\Relvz{\Psx{\Tsuml\Tta\Ttb}}$, either \begin{enumerate} \item R-Label with $\Ahi\proves\Lt\not\sle\Rell$: by R-Label and R-Term. \item R-Inl with $\Vtz=\Einlx\Vt$ and $\Vtzp=\Einlx\Vtp$ with $\Relvx{\Psx\Tta}$: by EM-Trans with E-CaseInl, \begin{eqnarray*} \Evalmx{\Ecase\Vtz{\Epsx\Vta}{\Epsx\Vtb}} {\Eapp{\Epsx\Vta}\Vt} \\ \Evalmx{\Ecase\Vtzp{\Epsxp\Vtap}{\Epsxp\Vtbp}} {\Eapp{\Epsxp\Vtap}\Vtp} \end{eqnarray*} By Esu-App, Tsu-Fun, Lemma~\ref{lem:subs-join} (substitution for join) and R-Fun, we have \[ \Reley{(\Eapp{\Epsx\Vta}\Vt)}{(\Eapp{\Epsxp\Vtap}\Vtp)} {\Psx{\join\Ttz\Lt}}\] By R-Term, we have related values for the two application terms. By EM-Trans, we have related values for the result terms. \item R-Inr with $\Vtz=\Einrx\Vt$ and $\Vtzp=\Einrx\Vtp$: symmetric to the previous case. \end{enumerate} \item T-Fun: \setcounter{equation}0 $\Rule{\Typey\Etz\Ttb & \Ev\not\in\dom\Eenv & \LabelD{\Lt}} {\Typex{\Efunx\Tta\Etz}{\Tfunl\Tta\Ttb}}$ $\Ev\not\in\dom\Es$ because $\Ev\not\in\dom\Eenv$. By Esu-Fun, Tsu-Fun and Lemma~\ref{lem:subs-join} (substitution for join), \begin{eqnarray} \Epsx{\Efunx\Tta\Etz} &=& \Efun\Ev{\Psx\Tta}{\Epsx\Etz} \\ \Epsxp{\Efunx\Tta\Etz} &=& \Efun\Ev{\Psx\Tta}{\Epsxp\Etz} \\ \Psx{\Tfunl\Tta\Ttb} &=& \Tul{(\Tfun{\Psx\Tta}{\Psx\Ttb})}{\Psx\Lt} \\ \join{\Psx\Ttb}{\Psx\Lt} &=& \Psx{\join\Ttb\Lt} \end{eqnarray} By (1)-(4), EM-Refl, R-Fun and R-Term, it remains to show that $\forall\Relvx{\Psx\Tta}$, \[ \Rele{(\Eapp{(\Efun\Ev{\Psx\Tta}{\Epsx\Etz})}\Vt)} {(\Eapp{(\Efun\Ev{\Psx\Tta}{\Epsxp\Etz})}\Vtp)} {\Psx{\join\Ttb\Lt}}\Rell \] By EM-Trans with E-AppFun, \begin{eqnarray} \Evalmx{\Eapp{(\Efun\Ev{\Psx\Tta}{\Epsx\Etz})}\Vt}{\Subs\Ev\Vt{\Epsx\Etz}} \\ \Evalmx{\Eapp{(\Efun\Ev{\Psx\Tta}{\Epsxp\Etz})}\Vtp}{\Subs\Ev\Vtp{\Epsxp\Etz}} \end{eqnarray} Let $\Esz=\Es,\Ev\mapsto\Vt$ and $\Eszp=\Esp,\Ev\mapsto\Vtp$ such that \begin{eqnarray} \Subs\Ev\Vt{\Epsx\Etz}=\Epszx\Etz \\ \Subs\Ev\Vt{\Epsxp\Etz}=\Epsxzp\Etz \\ \Relg\Esz\Eszp\Rell{\Psx{\Eenv,\Ev:\Tta}} \end{eqnarray} By IH with Z-DModel and Z-IfDel and (9), $\Reley{\Epszx\Etz}{\Epsxzp\Etz}{\Psx{\join\Ttb\Lt}}$. Then, the result follows by (5)-(8) and R-Term. \item T-App: $\Rule{\Typex\Eta{\Tfunl\Tta\Ttb} & \Typex\Etb\Tta} {\Typex{\Eapp\Eta\Etb}{\join\Ttb\Lt}}$ By IH on $\Eta$ and $\Etb$, \begin{enumerate} \item $\Reley{\Epsx\Eta}{\Epsxp\Eta}{\Psx{\Tfunl\Tta\Ttb}}$ with $\Evalmx{\Epsx\Eta}\Vta$ and $\Evalmx{\Epsxp\Eta}\Vtap$ \item $\Reley{\Epsx\Etb}{\Epsxp\Etb}{\Psx\Tta}$ with $\Evalmx{\Epsx\Etb}\Vtb$ and $\Evalmx{\Epsxp\Etb}\Vtbp$ \end{enumerate} The result then follows by R-Fun and R-Term. \item T-PName: $\Rule{\LabelD{\Lt}}{\Typex\Epx{\Tpl\Lx}}$ By Esu-PName and Tsu-PName, $\Epsx\Et=\Epsxp\Et=\Epx$ and $\Psx{\Tpl\Lx}=\Tpl{\Psx{\Lx}}$. The result then follows by EM-Refl, R-PName and R-Term. \item T-IfDel: $\Rule{ \Typex\Eta{\Tpl\Lpa} & \Typex\Etb{\Tpl\Lpb} & \Type{\Penv,\Lpa\delto\Lpb}{\Eenv}{\Etc}{\Ttz} & \Typex\Etd\Ttz} {\Typex{\Eif\Eta\Etb\Etc\Etd}{\join\Ttz\Lt}}$ By IH on $\Eta$, $\Etb$, $\Etc$ and $\Etd$, \begin{enumerate} \item $\Reley{\Epsx\Eta}{\Epsxp\Eta}{\Psx{\Tpl\Lpa}}$ with $\Evalmx{\Epsx\Eta}\Vta$ and $\Evalmx{\Epsxp\Eta}\Vtap$ \item $\Reley{\Epsx\Etb}{\Epsxp\Etb}{\Psx{\Tpl\Lpb}}$ with $\Evalmx{\Epsx\Etb}\Vtb$ and $\Evalmx{\Epsxp\Etb}\Vtbp$ \item $\Reley{\Epsx\Etc}{\Epsxp\Etc}{\Psx\Ttz}$ with $\Evalmx{\Epsx\Etc}\Vtc$ and $\Evalmx{\Epsxp\Etc}\Vtcp$ \item $\Reley{\Epsx\Etd}{\Epsxp\Etd}{\Psx\Ttz}$ with $\Evalmx{\Epsx\Etd}\Vtd$ and $\Evalmx{\Epsxp\Etc}\Vtdp$ \end{enumerate} By Esu-Case and EM-Trans with E-Case, \begin{eqnarray*} \Epsx{\Eif\Eta\Etb\Etc\Etd} &=& \Eif{\Epsx\Eta}{\Epsx\Etb}{\Epsx\Etc}{\Epsx\Etd} \\ \Epsxp{\Eif\Eta\Etb\Etc\Etd} &=& \Eif{\Epsxp\Eta}{\Epsxp\Etb}{\Epsxp\Etc}{\Epsxp\Etd} \\ \Ahi,\Eif{\Epsx\Eta}{\Epsx\Etb}{\Epsx\Etc}{\Epsx\Etd} &\evalm& \Ahi,\Eif\Vta\Vtb{\Epsx\Etc}{\Epsx\Etd} \\ \Ahi,\Eif{\Epsxp\Eta}{\Epsxp\Etb}{\Epsxp\Etc}{\Epsxp\Etd} &\evalm& \Ahi,\Eif\Vtap\Vtbp{\Epsxp\Etc}{\Epsxp\Etd} \end{eqnarray*} By Tsu-PName and the inversion of $\Relva{\Psx{\Tpl\Lpa}}$ and $\Relvb{\Psx{\Tpl\Lpb}}$, either \begin{enumerate} \item R-Label with $\Ahi\proves\Lt\not\sle\Rell$: by R-Label, we have related values for the result terms. \item R-PName, R-PName with $\Vta=\Vta=\Ep{\Psx\Lpa}$, $\Vtb=\Vtbp=\Ep{\Psx\Lpb}$: if $\Actsfora{\Psx\Lpa}{\Psx\Lpb}$, then by EM-Trans with E-IfDel3, \begin{eqnarray*} \Evalmx{\Eif\Vta\Vtb{\Epsx\Etc}{\Epsx\Etd}}{\Epsx\Etc} \\ \Evalmx{\Eif\Vtap\Vtbp{\Epsxp\Etc}{\Epsxp\Etd}}{\Epsxp\Etc} \end{eqnarray*} Otherwise, if $\NotActsfora{\Psx\Lpa}{\Psx\Lpb}$, then by EM-Trans with E-IfDel4, \begin{eqnarray*} \Evalmx{\Eif\Vta\Vtb{\Epsx\Etc}{\Epsx\Etd}}{\Epsx\Etd} \\ \Evalmx{\Eif\Vtap\Vtbp{\Epsxp\Etc}{\Epsxp\Etd}}{\Epsxp\Etd} \end{eqnarray*} In both cases, by EM-Trans, we have related values for the result terms at type $\Psx\Ttz$. By Proposition~\ref{prop:join} (join order) and Lemma~\ref{lem:subs-sub-full} (substitution for subtyping), they are also related at type $\Psx{\join\Ttz\Lt}$. The result then follows by R-Term. \end{enumerate} \item T-All: \setcounter{equation}0 $\Rule{\Type{\Penv,\Lv\delto\Lp}{\Eenv}\Etz\Ttz & \Lv\not\in\dom\Penv & \LabelD{\Lt}} {\Typex{\Eallxp\Etz}{\Tallxpl\Ttz}}$ $\Lv\not\in\dom\Es$ because $\Lv\not\in\Penv$. By Esu-All, Tsu-All and Lemma~\ref{lem:subs-join} (substitution for join), \begin{eqnarray} \Epsx{\Eallx\Lp\Etz} &=& \Eall\Lv{\Psx\Lp}{\Epsx\Etz} \\ \Epsxp{\Eallx\Lp\Etz} &=& \Eall\Lv{\Psx\Lp}{\Epsxp\Etz} \\ \Psx{\Tallxp\Ttz} &=& \Tul{(\Tallxp{\Psx\Ttz})}{\Psx\Lt} \\ \join{\Psx\Ttz}{\Psx\Lt} &=& \Psx{\join\Ttz\Lt} \end{eqnarray} By (1)-(4), EM-Refl, R-All and R-Term, it remains to show that $\forall\Actsfora\Lx{\Psx\Lp}$, \[ \Rele{(\Epapp{(\Eall\Lv{\Psx\Lp}{\Epsx\Etz})}\Lx)} {(\Epapp{(\Eall\Lv{\Psx\Lp}{\Epsxp\Etz})}\Lx)} {\Psx{\join\Ttz\Lt}}\Rell \] By EM-Trans with E-PAppAll, \begin{eqnarray} \Evalmx{\Epapp{(\Eall\Lv{\Psx\Lp}{\Epsx\Etz})}\Lx}{\Subs\Lv\Lx{\Epsx\Etz}} \\ \Evalmx{\Epapp{(\Eall\Lv{\Psx\Lp}{\Epsxp\Etz})}\Lx}{\Subs\Lv\Lx{\Epsxp\Etz}} \end{eqnarray} Let $\Psz=\Ps,\Lv\mapsto\Lx$ such that \begin{eqnarray} \Subs\Lv\Lx{\Epsx\Etz}=\Es\Psxz\Etz \\ \Subs\Lv\Lx{\Epsxp\Etz}=\Esp\Psxz\Etz \\ \Mod\Psz{\Penv,\Lv\delto\Lp} \end{eqnarray} By IH with Z-IfDel, (13) and Z-RSubs, $\Reley{\Epsx\Etz}{\Epsxp\Etz}{\Psx{\join\Ttz\Lt}}$. Then, the result follows by (7)-(12) and R-Term. \item T-PApp: $\Rule{\Typex\Etz{\Tallxpl\Ttz}} {\Typex{\Epapp\Etz\Lp}{\join\Ttz\Lt}}$ By IH on $\Etz$, we have $\Reley{\Epsx\Etz}{\Epsxp\Etz}{\Psx{\Tallxpl\Ttz}}$ with $\Evalmx{\Epsx\Etz}\Vt$ and $\Evalmx{\Epsxp\Etz}\Vtp$. The two principals on the right are both $\Psx\Lpa$ and, by $\Actsfora\Lpa\Lpb$ and Lemma~\ref{lem:subs-sub-full}, we have $\Actsfora{\Psx\Lpa}{\Psx\Lpb}$. The result then follows by R-All and R-Term. \item T-Sub: $\Rule{\Typex\Etz\Tta & \Stypex\Tta\Ttb} {\Typex\Etz\Ttb}$ By IH on $\Etz$, we have $\Reley{\Epsx\Etz}{\Epsxp\Etz}{\Psx\Tta}$ with $\Evalmx{\Epsx\Etz}\Vt$ and $\Evalmx{\Epsxp\Etz}\Vtp$. The result then follows by Lemma~\ref{lem:sub-logical} (subtyping for logical relations) and R-Term. \end{itemize} \end{proof} \end{document}