% -*- LaTeX -*- \documentclass{llncs} \usepackage{hyperref,url,euler,proof,makeidx,comment} \usepackage{amstext,amssymb,amsmath,multicol,longtable} \newif\iftechreport \techreportfalse \newif\ifjournal \journalfalse \iftechreport\makeindex\fi \newtheorem{thm}{Theorem} \newtheorem{lem}[thm]{Lemma} \newtheorem{col}[thm]{Corollary} \newtheorem{eg}[thm]{Example} \newcommand{\N}[1]{\text{\rm\ttfamily\mdseries{#1}}} \newcommand{\Infer}[2]{\infer{#2}{#1}} \newcommand{\eval}[1]{\xrightarrow{\;#1\;}} \newcommand{\evalm}[1]{{\xrightarrow{\;#1\;}\hspace{-1ex}{}^*\;}} \newcommand{\evalw}[0]{{\xrightarrow{\;@\not<:z@\;}\hspace{-1ex}{}^\omega\;}} \newcommand{\evaln}[1]{{\stackrel{@z@}\Longrightarrow\hspace{-1ex}{}^{\;#1}\;}} \newcommand{\eqm}[0]{\stackrel{@.@}\approx} \newcommand{\eqv}[0]{\stackrel{@.@}\sim} \newcommand{\nprime}[0]{\N{'}} \newcommand{\zspace}[0]{\;} \newcommand{\kindl}{\mathcal{L}} \newcommand{\kindp}{\mathcal{P}} \newcommand{\kindj}{\mathcal{J}} \newcommand{\Rulez}[3]{\infer{#3}{#2}} \newcommand{\Class}[2]{\fbox{\N{#2} ::= $\cdots$} & \fbox{#1}\index{#1}} \newcommand{\Def}[3]{\fbox{\N{#2} $\equiv$ {#3}} & \fbox{#1}\index{#1}} \newcommand{\Syntax}[3]{#3 ::= #2 & \text{(#1)}\index{#1}} \newcommand{\Scheme}[2]{\fbox{#2} & \fbox{#1}\index{#1}} \newcommand{\Axiom}[2]{{#2} & \text{(#1)}\index{#1}} \newcommand{\Axiomz}[2]{{#2}} \newcommand{\Rule}[3]{\infer{#3}{#2} & \raisebox{1.5ex}{\text{(#1)}}\index{#1}} \newcommand{\Thm}[3]{\fbox{\Infer{#2}{#3}} & \fbox{#1}\index{#1}} \newcommand{\Proof}[2]{{#2} & \text{(#1)}\index{#1}} \title{A Design for a Security-typed Language with Certificate-based Declassification} \author{Stephen Tse \qquad Steve Zdancewic} \institute{University of Pennsylvania \iftechreport \\ Technical report: MS-CIS-04-16 \fi} \begin{document} \maketitle % {\let\tmp=\thefootnote\renewcommand{\thefootnote}{}\footnote{ % Stephen Tse {\tt } and Steve % Zdancewic {\tt }. % %Submitted to POPL, 2004. % Last update: \today. % }\addtocounter{footnote}{-1}\let\thefootnote=\tmp} \begin{abstract} This paper presents a calculus that supports information-flow security policies and certificate-based declassification. The decentralized label model and its downgrading mechanisms are concisely expressed in the polymorphic lambda calculus with subtyping (System @F_{<:}@). We prove a conditioned version of the noninterference theorem such that authorization for declassification is justified by digital certificates from public-key infrastructures. \end{abstract} \section{Introduction} Information-flow policies constrain the propagation of confidential data and provide an end-to-end guarantee of security. {\em Security-typed languages} have become a promising approach for specifying and enforcing such policies with static type systems~\cite{myers03jc}. However, designing a {\em safe} and {\em secure} information-flow type system is still a challenging problem: programmers want to express fine-grained security policies with advanced types, but reasoning about security guarantees in such complex systems is non-trivial. This paper presents a security-typed language with well-studied constructs from the polymorphic lambda calculus with subtyping (System @F_{<:}@)~\cite{curien92}. Language features such as labels and effects are isolated in a monadic style. This design makes typing and evaluation rules easy to understand and the proofs of {\em type-safety} and {\em noninterference} modular. Another challenge of designing a security-typed language is to provide downgrading mechanisms that intentionally break the security guarantees, if such actions can be justified externally. Downgrading mechanisms, such as {\em delegating} to another principal or {\em declassifying} secret data, are important in practical programming~\cite{zdancewic02thesis}. The decentralized label model by Myers and Liskov~\cite{myers97sosp} addresses this problem and introduces the notions of principals and reader sets to statically track the authority for downgrading. One of our design decisions is to treat labels, principals and downgrading privileges uniformly as types so that the decentralized label model can be integrated easily into our language. For example, subtyping naturally models principal delegation, while intersection and union types give rise to principal groups and label refinements. A security language with these encodings allows expressive, decentralized policies, yet the semantics remains easy to understand. Our previous work~\cite{tse04sp} connects the static security type system with run-time security mechanisms such as public-key infrastructures. The language there uses {\em singleton types} such that a principal is represented as a public key, and the authority of a principal granting a privilege is represented as a digital certificate. We improve on our previous work with monads and subtyping, allowing us to prove a conditioned version of noninterference even in the presence of declassification (which was neither stated nor proved before). In particular, we formalize downgrading mechanisms such as delegation and declassification as subtyping, and certificate verification as {\em extending} the subtyping relation. More importantly, the conditioned noninterference now captures the intuition that certificates externally justify the information leaks due to declassification. The main contributions of our paper are: \begin{enumerate} \item the design of a safe and secure information-flow type system with bounded quantification and effects in a monadic style; \item the integration of the decentralized label model with type constructors and the use of subtyping to model delegation, declassification, and endorsement; \item a conditioned version of the noninterference theorem that justifies certificate-based declassification. \end{enumerate} The work here subsumes our previous work~\cite{tse04sp}, adding existential types, run-time labels and privileges, and a conditioned noninterference theorem for the full language. We have also built a prototype interpreter called {\em Apollo}\footnote{The interested reader is invited to visit \url{http://www.cis.upenn.edu/~stse/apollo}.}. \iftechreport For brevity, the main body of this paper only shows the interesting cases of rules and proofs. The full details are in the appendix. \else For brevity, this paper shows only the interesting cases of rules and proof. Our technical report~\cite{tse04esop-tr} contains all rules and proofs of type-safety and noninterference for the full language. The proof of type-safety is also mechanically formalized and checked with Twelf (a logical framework). \fi The rest of the paper is organized as follows. Section~\ref{sec:core} starts with a core calculus with labels to study noninterference and extends it with effects. Section~\ref{sec:dlm} introduces the decentralized label model and shows how the core calculus supports the notion of principals, confidentiality and integrity. Furthermore, downgrading mechanisms are studied as subtyping, and certificate-based declassification is justified using constructs from public-key infrastructures. The paper then discusses related work in Section~\ref{sec:relate} and concludes in Section~\ref{sec:con}. \section{Core label calculus} \label{sec:core} Let us start by introducing a core calculus with monadic labels and effects for analyzing program dependency. This section proves two important security theorems, {\em type-safety} and {\em noninterference}, for our core calculus. \subsection{Monadic labels} \label{sec:label} The first part of our label calculus is based on the dependency core calculus (DCC)~\cite{abadi99popl} and the polymorphic lambda calculus with subtyping (System @F_{<:}@)~\cite{curien92}. The motivation behind DCC is to use {\em monadic labels} as a unifying framework to study many important program analyses such as binding time, information flow, slicing, and function call tracking. DCC uses a lattice of monads and a special typing rule for their associated bind operations to describe the dependency of computations in a program. Unlike DCC, which is based on the {\em call-by-name} simply-typed lambda calculus, our core calculus is based on the {\em call-by-value}\/ @F_{<:}@. Our work should apply also to call-by-name languages; we pick call-by-value semantics simply because of our familiarity. The features of @F_{<:}@ will become essential in later sections: bounded quantification (@all a<:t.t@ and @some a<:t.t@) are used to connect static security policies and run-time public-key infrastructures (Sect.~\ref{sec:cert}), and subtyping is used to model principal delegations and policy refinements (Sect.~\ref{sec:confi}). The following grammar defines the syntax for our basic types and terms: % {\small\[\begin{array}{rcl} @t@ &::=& @<> | | t+t | t->t | top_k | bot_k | a | all a<:t.t | some a<:t.t@ \\[1ex] @m@ &::=& @<> | | prj1 m | prj2 m | inj1 m | inj2 m | case m m m | x | fun x:t.m | m m@ \\ && @| poly a<:t.m | m[[t]] | pack (t,m) as t | open (a,x)=m in m@ \end{array}\]}% % The types consists of unit, products, sums, functions, top, bottom, variables, universal and existential quantification, while the terms consists of unit, products, projections, injections, cases, variables, functions, applications, type abstractions and instantiations, and package packings and openings. We also encode Booleans @bool@ using unit and sums. The types top @top_k@ and bottom @bot_k@ are annotated by a kind @k@: types $\mathcal{T}$, labels $\mathcal{L}$, principals $\mathcal{P}$, and privileges $\mathcal{J}$. Principals and privileges will be explained in Sect.~\ref{sec:dlm} with the decentralized label model. One of our design choices is to identify these syntactic classes (types @t@, labels @l@, principals @p@, and privileges @j@): % {\small\[ @t@ \equiv @l@ \equiv @p@ \equiv @j@ \qquad\qquad @k@ ::= \mathcal{T\ |\ L\ |\ P\ |\ J} \]}% % This design allows the reuse of type machinery, such as polymorphism and subtyping, uniformly for these concepts. We will see this benefit again for intersection and union types in Sect~\ref{sec:confi}, and singleton types in Sect.~\ref{sec:cert}. % We use the semantics of Kernel @F_{<:}@~\cite{curien92}. The evaluation judgment is denoted by @m --> m@\label{judge:ev}, the typing judgments by @d;g |- m : t@\label{judge:ty}, and the subtyping judgment by @d |- t <: t@\label{judge:sty}, where @d@ is a type context and @g@ is a term context. We follow Pottier's notation~\cite{pottier02popl} for specifying the subtyping polarities @oo@ of type constructors: @o+@ for covariant, @o-@ for contravariant, and @o.@ for invariant: % {\small\[\begin{array}{rcl} @d@ &::=& @empty | d,a<:t@ \qquad @g@ ::= @empty | g,x:t@ \\ @oo@ &::=& @ | o+ + o+ | o- -> o+ | all a<:o..o+ | some a<:o..o+@ \end{array}\]}% % We omit rules for the standard @F_{<:}@ constructs above and focus on the new types and terms for labels: monadic types @t[l]@ (indexed by labels @l@), and their corresponding units @m[l]@ and @bind@ operator. % {\small\[\begin{array}{rcl\@{\qquad}rcl\@{\qquad}rcl} @t@ &::=& @.. | t[l]@ & @m@ &::=& @.. | m[l] | bind x=m in m@ & @oo@ &::=& @.. | o+[o+]@ \end{array}\]}% Syntactically, these label constructs have the highest precedence such that @m1 m2[l]@ means @m1 (m2[l])@. We write high and low labels as $\N{H} = \top_{\mathcal{L}}$ and $\N{L} = \bot_{\mathcal{L}}$. The subtyping relation of labels @d |- l <: l@ forms a lattice and hence our language has a lattice of monads @t[l]@ and @m[l]@. Since labels and types are in the same syntactic class, we use a kinding judgment @d |- t :: k@ to rule out ill-formed types such as @bool -> H@ or @bool [bool]@. We omit the straight-forward kind system here; our technical report~\cite{tse04esop-tr} contains the full details. Now, let us see how the type system prevents low-level computation from depending on high-level computation: % {\small\[\begin{array}{c\@{\qquad}c} \Rulez{T-Lab} {@d;g |- m : t@ & @d |- l :: \kindl@} {@d;g |- m[l] : t[l]@} & \Rulez{T-Bind} {@d;g |- m1 : t1[l]@ & @d;g,x:t1 |- m2 : t2@ & @d |- l << t2@} {@d;g |- bind x=m1 in m2 : t2@} \end{array}\]}% % The label monad @m[l]@ marks the computation @m@ with the label @l@, restricting how it interacts with the rest of the program. The term @bind x = m1 in m2@ exposes the computation @m1@ protected inside the label type @t[l]@ to the scope of @m2@. Note that these typings are standard for monadic types, except that the return type of @bind@ here has type @t2@, rather than the expected type @t2[l]@. Instead, by connecting the subtyping of labels (@d |- l1 <: l2@) with the subtyping of types (@d |- t1 <: t2@), the following label protection judgment @d |- l << t@ ensures that the result of @bind@ still protects the data: % {\small\[\begin{array}{c\@{\qquad\qquad}c\@{\qquad\qquad}c} \Axiomz{P-Unit}{@d |- l << <>@} & \Rulez{P-Lab1}{@d |- l2 <: l1@} {@d |- l2 << t [l1]@} & \Rulez{P-Lab2}{@d |- l2 << t@} {@d |- l2 << t [l1]@} \end{array}\]}% % The unit type protects all labels as there is only one term of such type. Sum types, as information can be leaked by their tags, do not protect any label. The full set of rules also includes cases for products, functions, and universal types. \begin{eg} The term \quad @fun x:bool[H]. bind y = x in if y then 0 else 1@\quad is {\em not} well-typed, because @d |- H \not<< int@. An integer leaks information just like a Boolean or a sum. In contrast, \quad @fun x:bool[H]. bind y = x in if y then 0[H] else 1[H]@\quad {\em is} well-typed, because @d |- H << int[H]@.\qed \end{eg} Operationally, the label monad @m[l]@ evaluates the term inside until it is a value @v[l]@, while @bind@ evaluates @m1@ to a value @v[l]@ and substitutes @v@ for @x@ in @m2@. We specify the dynamic semantics by the following syntactic classes of values @v@ and evaluation contexts @E@~\cite{wright94ic}, and by small-step computation rules. We use @m[v/x]@ to denote the capture-free substitution of @v@ for @x@ in @m@. % {\small\[\begin{array}{rcl\@{\qquad\qquad}c} @v@ &::=& @.. | v[l]@ \\ @E@ &::=& @.. | E[l] | bind x=E in m@ & \Axiomz{E-Bind}{@bind x=v[l] in m --> m[v/x]@} \end{array}\]}% DCC also has fixpoints and pointed types. In the technical report, we add such features to the full language and prove noninterference using a bisimulation-like technique. For the lack of space, however, such development is left out here. \subsection{Security theorems} \label{sec:thm} Before we go on to enrich the language with features such as effects and the decentralized label model, let us state and prove two important theorems that guarantee the security of programs written in our language. These theorems still hold for our full languages (modulo some condition to account for declassification, to be explained in Sect.~\ref{sec:cert}); however, we prove them here for the core calculus first to demonstrate the proof techniques. By presenting and proving for the full language incrementally, we hope to substantiate our claim that monadic types make the design and proofs more modular. The first theorem is the type-safety of the language, which we have proved using the progress and preservation theorems. Type-safety states that a closed, well-typed program will not get stuck or generate any error. A closed program means that both the type and term contexts are empty, that is, @d=g=empty@. \begin{thm}[Progress and preservation]\label{thm:type-safe} If @empty;empty |- m1 : t@, then either @m1=v@ or @m1 --> m2@. And, if @d;g |- m1 : t@ and @m1 --> m2@, then @d;g |- m2 : t@. \end{thm} \begin{proof} By induction on the typing derivation~\cite{curien92,abadi99popl}.\qed \end{proof} The second theorem is the noninterference property of the language~\cite{myers03jc}, which states that if a program is well-typed, a low-level observer cannot distinguish between different high-level computations. The theorem requires a model of {\em observers} @z@ for specifying what information leaks are possible. Our model here is that, given an equivalence relation over values of the same type, a well-typed observer cannot distinguish {\em equivalent values}, which are parameterized by the security label of the observer. For example, we should have these equivalences for Booleans: % {\small\[\begin{array}{rclcl\@{\qquad}rclcl\@{\qquad}rclcl} @true@ &@~z@& @true@ &:& @bool@ & @true@ &@\not~z@& @false@ &:& @bool@ & @true[H]@ &@~l@& @false[H]@ &:& @bool[H]@ \end{array}\]}% % The first two say that no observer @z@ cannot distinguish @true@ from @true@, but an observer can tell the difference between @true@ and @false@. More interestingly, the third says that if values are protected inside the high monad, then different values become indistinguishable to the low-level observer @L@. Based on the intuition above, we generalize the equivalence relation in the following ways: (1) extend the relation to be higher-order, to account for functions; (2) parameterize the relation with arbitrary labels; (3) cover all types and values in the relation; and, (4) lift the relation from values to terms by evaluation. Formally, this logical equivalence relation is defined by the following rules. We denote the equivalence relation for closed values at closed type @t@ by @v ~z v : t@, and that for closed terms by @m ~~z m : t@\label{judge:eq}: % {\small\[\begin{array}{c\@{\qquad}c} \Rulez{R-Term}{@m1 -->* v1@ & @m2 -->* v2@ & @v1 ~z v2 : t@} {@m1 ~~z m2 : t@} & \Rulez{R-Fun}{@all (v3 ~z v4 : t1). v1 v3 ~~z v2 v4 : t2@} {@v1 ~z v2 : t1 -> t2@} \\\\ \Rulez{R-Lab1}{@v1 ~z v2 : t@} {@v1[l] ~z v2[l] : t[l]@} & \Rulez{R-All} {@all (t2 <: t1). v1[[t2]] ~~z v2[[t2]] : t[t2/a]@} {@v1 ~z v2 : all a<:t1. t@} \\\\ \Rulez{R-Lab2}{@l \not<: z@} {@v1[l] ~z v2[l] : t[l]@} & \Rulez{R-Some} {@v1 ~z v2 : t[t1/a]@} {@pack (t1,v1) ~z pack (t1,v2) : some a<:t2.t@} \end{array}\]}% % For reference in proofs later, we name these rules (from top to bottom, left to right) R-Term, R-Lab1, R-Lab2, R-Fun, R-All, and R-Some (with type annotations inside the @pack@ terms elided). We slightly abuse the notation by using @all@ both for the object-level quantification types @all a<:t.t@ and for the meta-level quantification in logical relations. Note that we do not deal with parametricity of polymorphic functions~\cite{wadler89fpca} nor the behavioral equivalence of existential packages~\cite{pitts98icalp}. That is, our model assumes that an observer can differentiate different representations of polymorphic functions or different implementations of existential packages. This assumption simplifies the equivalence relations, and is the key difference between noninterference and parametricity. The last step is to model an arbitrary observer as an open term that contains free type variables and term variables, and model observations as type substitutions @w@ and term substitutions @r@, which are defined as: % {\small\[\begin{array}{rcl\@{\qquad\qquad}rcl} @w@ &::=& @empty | w,a|->t@ & @r@ &::=& @empty | r,x|->v@ \end{array}\]}% % A judgment @w |= d@\label{judge:tmodel} says that a type substitution models a type context: for all @a\in dom(w)=dom(d)@, if @w(a)=t1@ and @a<:t2 \in d@, then @t1@ is closed, has the same kind as @t2@, and @d |- t1<:t2@. Another judgment @r1 ~z r2 : w(g)@\label{judge:mmodel} says that two term substitutions are equivalent under a term context of closed types: for all @x\in dom(r1)=dom(r2)=dom(w(g))@, if @r1(x)=v1@, @r2(x)=v2@ and @x:t \in w(g)@, then @v1 ~z v2 : t@. With the logical relations and the substitutions above, we can formally state the main theorem of the core label calculus: related substitutions preserve the logical equivalence. In other words, an arbitrary observer cannot distinguish values higher in the lattice. \begin{thm}[Noninterference for terms]\label{thm:ni} If @d;g |- m : t@ and @w |= d@ and @r1 ~z r2 : w(g)@, then @w r1(m) ~~z w r2(m) : w(t)@. \end{thm} \begin{proof} By induction on the typing derivation. Case @bind@: We are given @d;g |- bind x=m1 in m2 : t2@. By inversion, we have @d;g |- m1 : t1[l]@ (*1) and @d;g,x:t1 |- m2 : t2@ (*2) and @d |- l << t2@ (*3). By induction hypothesis with (*1), we have {\small\[ @w r1(m1) ~~z w r2(m1) : w(t1[l])@ \]}% By inversion of R-Term, @w r1(m1) -->* v1@ (*4) and @w r2(m1) -->* v2@ (*5) and @v1 ~z v2 : w(t1[l])@. Subcase @w(l)<:z@: By the inversion of R-Lab1, @v1=v3[w(l)]@ and @v2=v4[w(l)]@ and @v3 ~z v4 : w(t1)@ (*6). We then extend the term substitutions as % {\small\[\begin{array}{rcl\@{\qquad}rcl} @r1'@ &=& @r1,x|->v3@ & @r2'@ &=& @r2,x|->v4@ \end{array}\]}% % such that, by (*6), @r1' ~z r2' : w(g,x:t1)@ (*7). By induction hypothesis with (*2,*7), {\small\[ @w r1'(m2) ~~z w r2'(m2) : w(t2)@ \]}% which means that @w r1(m2)[v3/x] ~~z w r2(m2)[v4/x] : w(t2)@ (*8). By (*4,*5), % {\small\[\begin{array}{cl\@{\qquad\qquad}cl} & @w r1(bind x=m1 in m2)@ & & @w r2(bind x=m1 in m2)@ \\ =& @bind x=w r1(m1) in w r1(m2)@ & =& @bind x=w r2(m1) in w r2(m2)@ \\ @-->*@& @bind x=v3[w(l)] in w r1(m2)@ & @-->*@& @bind x=v4[w(l)] in w r2(m2)@ \\ @-->@& @w r1(m2)[v3/x]@ & @-->@& @w r2(m2)[v4/x]@ \end{array}\]}% % Therefore, by R-Term and (*8), we conclude that @w r1(bind x=m1 in m2) ~~z w r2(bind x=m1 in m2) : w(t2)@. Subcase @w(l)\not<:z@: by Lemma~\ref{lem:prot} with (*3).\qed \end{proof} \begin{lem}[Noninterference for protected terms]\label{lem:prot} If @d |- l << t@, @w |= d@ and @w(l)\not<:z@, then @m1 ~~z m2 : t@.\qed \end{lem} \subsection{Monadic effects} \label{sec:effect} We now turn to study information flows in the presence of computational effects. Practical programs interact with external systems and produce effects; observers can then learn high-security values from those effects. To prevent information leaks through such channel, we need to refine the type system with effect types. We again use the monadic style of effect types~\cite{moggi89lics,crary04fcs}. The benefit of monads is that the new feature can be incrementally added to the language we have shown so far. That is, all the typing and evaluation rules in Section~\ref{sec:label} remain unchanged. Traditional approaches, in contrast, require tracking of effects in all typing rules, spreading the interaction of labels and effects everywhere. Monads also help in structuring proofs in a modular way, which will be explained for Theorem~\ref{thm:niexp}. For lazy languages like Haskell, we can simply add the IO monad. For eager languages like the one here, we need to introduce a new syntactic class @e@ for {\em effectful expressions} to distinguish from {\em pure terms} @m@ introduced in Sect.~\ref{sec:label}: % {\small\[\begin{array}{rcl\@{\qquad\quad}rcl} @t@ &::=& @.. | t ! q@ & @oo@ &::=& @.. | o+ ! o-@ \\ @e@ &::=& @return m | run x=m in e@ & @m@ &::=& @.. | e ! q@ \end{array}\]}% % Every top-level program is now an expression, instead of a term. We model effects as outputs at a given label @l@, which are visible to an observer of level @z@ if @l<:z@. An observer cannot tell the difference between effects of different labels, but can count the number of visible effects happening in the program. This treatment gives us a uniform way of modeling language features with effects and could be extended to effects that carry additional values. Experience with effectful languages suggests that this technique can be extended to memory references with reads and writes~\cite{crary04fcs}. Expressions are @return m@ and @run x=m in e@, which explicitly specify the order of execution. The term @e!q@ delays the effects @q@ in @e@ and thus can be considered pure, but has the monadic effect type @t!q@ (indexed by effect labels @q@). Here @q@ is a lower bound on the labels of observable effects happening in @e@, similar to the concept of {\em program counter} in the literature~\cite{myers03jc}. The typing judgment for expressions is @d;g |- e : t ! q@\label{judge:ety}, which says that under the type context @d@ and term context @g@, the expression @e@ has the monadic effect type @t ! q@. The following are the typing rules for the new constructs: % {\small\[\begin{array}{c\@{\quad}c} \Rulez{T-Ret} {@d;g |- m : t@} {@d;g |- return m : t ! H@} & \Rulez{T-Run} {@d;g |- m : t1!q@ & @d;g,x:t1 |- e : t2!q@} {@d;g |- run x=m in e : t2 ! q@} \\\\ \Rulez{T-Eff} {@d;g |- e : t ! q@ & @d |- q :: \kindl@} {@d;g |- e ! q: t ! q@} & \Rulez{P-Eff}{@d |- l << t@ & @d |- l <: q@} {@d |- l << t ! q@} \end{array}\]}% The expression @return m@ has no effect and hence its type is given the empty effect @H@. We interpret the effect at @H@ to be visible to no-one, while the effect at @L@ to be visible to everyone. The expression @run x=m in e@ executes the encapsulated effect of @m@, and then continue with @e@. Both @m@ and @e@ have the same effect type @q@; otherwise, the subsumption rule of subtyping can be used. The bottom left rule simply connects the typing judgments of terms and expressions. The bottom right rule, on the other hand, is an additional label protection judgment (defined in Sect.~\ref{sec:core}) for effect types. The rule says that the underlying type must protect the label and the computation must generate effects higher than the label. In other words, once the program has bound high-security data, it may not produce low observable effects. \begin{eg} The expression \quad {\small@run zz = (bind y = x in if y then c!H else c!L) in zz@}, \quad where @c \equiv return <>@ and @x:bool[H]@, is insecure. This is a typical example of {\em implicit information flow through program counter} in the literature~\cite{myers03jc}, where a program leaks information about a high-security Boolean through side effects. \end{eg} The evaluation judgment for expressions is @e ==>q e@\label{judge:evm}, where @q@ is the side effect during such step. We use @u@ to denote the values for expressions: % {\small\[\begin{array}{c} @u@ ::= @return v@ \qquad\qquad @v@ ::= @.. | e ! q@ \\ @E@ ::= @.. | return E | run x=E in e | run x=(return E)!q in e@ \\[1ex] \Axiomz{E-Run}{@run x=(return v)!q in e ==>q e[v/x]@} \end{array}\]}% % Since the congruence rules for expressions have no computational effects, we can still use evaluation contexts @E@ to describe the evaluation order of expressions. The term @e!q@ is a value because it is a closure that delays computation. \begin{eg} The following expression of type @bool ! L@ evaluates as: {\small\[\begin{array}{cl} & @run x = (run y = (return prj2 )!L in return y)!H in return x@ \\ @-->@ & @run x = (run y = (return false)!L in return y)!H in return x@ \\ @==>{L}@ & @run x = (return y)[false/y]!H in return x@ \\ @=@& @run x = (return false)!H in return x@ \\ @==>{H}@ & @(return x)[false/x]!H@ \\ @=@& @return false@ \hfill\qed \end{array}\]}% \end{eg} To model that an observer can now distinguish programs due to computational effects, we need the following new equivalence judgments for effectful expressions and values: @e ~~z e : t ! q@ and @u ~z u : t ! q@\label{judge:eeq}. The rules for expressions make use of a new evaluation relation, @e -=>{n} u@, which is explained below. % {\small\[\begin{array}{cr\@{\qquad\quad}cr} \Rule{R-Eff}{@e1 ~~z e2 : t!q@} {@e1!q ~z e2!q : t!q@} & \Rule{R-Ret}{@v1 ~z v2 : t@} {@return v1 ~z return v2 : t!q@} \end{array}\]} % {\small\[\begin{array}{cr} \Rule{R-Exp} {@e1 -=>{n} u1@ & @e2 -=>{n} u2@ & @u1 ~z u2 : t!q@} {@e1 ~~z e2 : t!q@} \end{array}\]}% % The rules on the top simply connect the term equivalence and the expression equivalence. Expressions are equivalent, the bottom rule says, if they produce the same number of effects visible to the observer and halt at equivalent values. To formalize such equivalence, we first classify evaluation steps into those that are {\em visible} and those that are {\em invisible} to the observer\label{judge:evmx}. Then, a visible evaluation step can be prefixed and suffixed with any number of invisible evaluation steps. % {\small\[\begin{array}{rcl\@{\qquad\qquad}rcl\@{\qquad\qquad}rcl} @==>{<:z}@ &\equiv& @\bigcup_{q<:z} ==>q@ & @==>{\not<:z}@ &\equiv& @\bigcup_{q\not<:z} ==>q@ & @-=>{}@ &\equiv& @==>*{\not<:z} \circ ==>{<:z} \circ\ ==>*{\not<:z}@ \end{array}\]}% % The evaluation judgment we want is therefore the @n@-step closure @-=>{n}@ of @-=>{}@. Note that @==>*{\not<:z} \circ ==>{<:z}@ is the composition of the two relations, while @==>*{\not<:z}@ is the reflexive and transitive closure of @==>{\not<:z}@. Having refined our observer model as above, we proceed to proving noninterference for our core calculus with expressions. The main idea is to track the number of visible effects produced during the evaluation. Note that the following proof is complete yet short in length. Since the proof is by induction on the typing derivation, monadic types allow an incremental proof, because the original proof for Theorem~\ref{thm:ni} remains valid and requires only a simple extension for @e!q@. Here we can focus merely on the new typing rules for @return e@ and @run x=m in e@. \begin{thm}[Noninterference for expressions]\label{thm:niexp} If @d;g |- e : t ! q@ and @w |= d@ and @r1 ~z r2 : w(g)@, then @w r1(e) ~~z w r2(e) : w(t) ! w(q)@. \end{thm} \begin{proof} By mutual induction with Theorem~\ref{thm:ni} (extended with @e!q@) on the typing derivation. % Case @return@: We are given @d;g |- return m : t ! H@. By inversion, we have @d;g |- m : t@. By Theorem~\ref{thm:ni}, we have @w r1(m) ~~z w r2(m) : w(t)@. By inversion of R-Term, @w r1(m) -->* v1@ and @w r2(m) -->* v2@ and @v1 ~z v2 : w(t)@. Therefore, by R-Ret, we conclude that @w r1(return m) ~~z w r2(return m) : w(t) ! w(q)@. % Case @run@: We are given @d;g |- run x=m in e : t2 ! q@. By inversion, we have @d;g |- m : t1!q@ (*1) and @d;g,x:t1 |- e : t2!q@ (*2). By Theorem~\ref{thm:ni} with (*1), we have {\small\[ @w r1(m) ~~z w r2(m) : w(t1)!w(q)@ \]}% By inversion of R-Term, @w r1(m) -->* v1@ (*3) and @w r2(m) -->* v2@ (*4) and @v1 ~z v2 : w(t1)!w(q)@. By inversion of R-Eff, @v1=e1!w(q)@ and @v2=e2!q@ and @e1 ~~z e2 : w(t1)!w(q)@. By inversion of R-Exp, @e1 -=>{n} u1@ (*5) and @e2 -=>{n} u2@ (*6) and @u1 ~z u2 : w(t1):w(q)@. By inversion of R-Ret, @u1 = return v3!w(q)@ and @u2 = return v4!w(q)@. We then extend the term substitutions as % {\small\[\begin{array}{rcl\@{\qquad\qquad}rcl} @r1'@ &=& @r1,x|->v3@ & @r2'@ &=& @r2,x|->v4@ \end{array}\]}% % such that @r1' ~z r2' : w(g,x:t1)@ (*7). By induction hypothesis with (*2,*7), {\small\[ @w r1'(e) ~~z w r2'(e) : w(t2)!w(q)@ \]}% which means that @w r1(e)[v3/x] ~~z w r2(e)[v4/x] : w(t2)!w(q)@ (*8). By (*3,*4,*5,*6), % {\small\[\begin{array}{\@{\!\!}cl\@{\quad}cl} & @w r1(run x=m in e)@ & & @w r2(run x=m in e)@ \\ =& @run x=w r1(m) in w r1(e)@ & =& @run x=w r2(m) in w r2(e)@ \\ @-->*@& @run x=e1!w(q) in w r1(e)@ & @-->*@& @run x=e2!w(q) in w r2(e)@ \\ @-=>{n}@& @run x=(return v3)!w(q) in w r1(e)@ & @-=>{n}@& @run x=(return v4)!w(q) in w r2(e)@ \\ @==>q@& @w r1(e)[v3/x]@ & @==>q@& @w r2(e)[v4/x]@ \end{array}\]}% % That means {\small\[\begin{array}{rcl} @w r1(run x=m in e)@ &@-=>{n+i}@& @w r1(e)[v3/x]@ \\ @w r2(run x=m in e)@ &@-=>{n+i}@& @w r2(e)[v4/x]@ \end{array}\]}% % where @i=1@ if @q <: z@, or @i=0@ otherwise. By R-Exp and (*8), we conclude that @w r1(run x=m in e) ~~z w r2(run x=m in e) : w(t2)!w(q)@.\qed \end{proof} \ifjournal \subsection{Fixpoints and divergence} \label{sec:fix} The last feature we add to the core label calculus is fixpoints, which are important for recursive programming. Programs with fixpoints may diverge and our observer model cannot assume termination for testing the equivalence of terms any more (R-Term and R-Exp). Moreover, effects and divergence interact; an observer can distinguish an infinite loop with no effects from another loop that keeps producing effects. Again, our strategy is to extend our type system and equivalence relation to account for divergence in the presence of effects. Based on ideas from DCC~\cite{abadi99popl}, we add fixpoints @fix m@ and pointed types @t++@ to our core calculus in a call-by-value setting. Fixpoints for expressions @fix x.e@ allows us to write recursive programs producing effects~\cite{moggi03}. Variables @x@ is now overloaded to be both term variables and expression variables, and thus typing contexts @g@ are extended to handle typing for expression variables @g,x:t!q@. Pointed types are yet more monads that track possible divergence of the program~\cite{howard96icfp}. The unit @lift m@ injects the term @m@ into the monad, while the sequence operator @seq x=m1 in m2@ ensures the termination of first term before evaluating the second one: % {\small\[\begin{array}{rcl} @g@ &::=& @.. | g,x:t!q@ \\ @r@ &::=& @.. | r,x|->u@ \\ @t@ &::=& @.. | t++@ \\ @oo@ &::=& @.. | o+++@ \\\\ @m@ &::=& @.. | fix m | lift m | seq x=m in m@ \\ @e@ &::=& @.. | x | fix x:t!q.e@ \\ @v@ &::=& @.. | lift v@ \\ @E@ &::=& @.. | fix E | lift E | seq x=E in m@ \end{array}\]}% % {\small\[\begin{array}{cr} \Rule{T-Fix1} {@d; g |- m : t -> t@ & @d |- \dagger << t@} {@d; g |- fix m : t@} \\\\ \Rule{T-Var2} {@x:t!q \in g@} {@d; g |- x : t ! q@} \\\\ \Rule{T-Fix2} {@d; g,x:t!q |- e : t ! q@ & @d |- \dagger << t@} {@d; g |- fix x:t!q. e : t ! q@} \\\\ \Rule{T-Lift} {@d; g |- m : t@} {@d; g |- lift m : t++@} \\\\ % {@d; g |- m2 : t1++@ & @d;g,x:t1 |- m2 : t2@ & @d |- \dagger << t2@} \Rule{T-Seq} {\begin{array}{ll} @d; g |- m1 : t1++@ \\ @d;g,x:t1 |- m2 : t2@ & @d |- \dagger << t2@ \end{array}} {@d; g |- seq x=m1 in m2 : t2@} \\\\ \Axiom{E-Fix1} {@fix (fun x:t.m) --> m[fix (fun x:t.m)/x]@} \\\\ \Axiom{E-Fix2} {@fix x:t.e ==>top e[fix x:t.e/x]@} \\\\ \Axiom{E-Seq} {@seq x=lift v in m2 --> m2[v/x]@} \end{array}\]}% The only new judgment is pointed protection: @d |- \dagger << t@\label{judge:ppt}, which is defined similarly to the label protection @d |- l << t@: % {\small\[\begin{array}{cr} \Axiom{D-Div}{@d |- \dagger << t++@} \\\\ \Rule{D-Fun}{@d |- \dagger << t2@} {@d |- t1 -> \dagger << t2@} \end{array}\]}% \newcommand{\einf}[0]{\omega_{L}} \begin{eg} The following expression @\einf@ of type @<>++:L@ will produce an infinite sequence of outputs at @L@: {\small\[ @\omega_{L} = fix x:<>++!L. run y=(return <>)!L in x@\]}% {\small\[\begin{array}{cl} & \einf \\ @==>{top}@& @run y=(return <>)!L in\ \einf@ \\ @==>{L}@& @\einf[<>/y]@ \\ @=@& @\einf@ \\ @==>{top}@& @run y=(return <>)!L in\ \einf@ \\ @==>{L}@& @\einf[<>/y]@ \\ @..@& \end{array}\]}% \end{eg} The label protection rule for pointed types (see below) allows a choice between {\em strong noninterference} and {\em weak noninterference}, which determines whether the observer model is termination-sensitive. For both versions of noninterference, two terms are equivalent if they halt at equivalent values, or they both diverge. If one term halts while the other does not, the two terms are equivalent under weak noninterference, but not strong noninterference. Therefore, strong noninterference is termination-sensitive and implies weak noninterference, which is termination-insensitive. A pointed type does not protect any label at all under strong noninterference; weak noninterference, on the other hand, permits the following label protection rule [todo say p-weak is already in dcc paper]: % {\small\[\begin{array}{cr} \Rule{P-Weak}{@d |- l << t@} {@d |- l << t++@} \end{array}\]}% % According to the discussion above, we add the following rules for the value and the term equivalences. The predicate @-->^\omega@ is the omega-closure of @-->@, meaning that the program diverges and goes into an infinite loop. % {\small\[\begin{array}{cr} \Rule{R-Lift}{@v1 ~z v2 : t@} {@lift v1 ~z lift v2 : t@} \\\\ \Rule{R-Strong1}{@m1-->^\omega@ & @m2-->^\omega@} {@m1 ~~z m2 : t@} \\\\ \Rule{R-Weak1}{@m1-->^\omega@} {@m1 ~~z m2 : t@} \\\\ \Rule{R-Weak2}{@m2 -->^\omega@} {@m1 ~~z m2 : t@} \end{array}\]}% % Similarly, we add the rules for effectful expressions and their values. The predicate @\evalw@ is the omega-closure of @==>{\not<:z}@ (which is defined in Sect.~\ref{sec:effect}), meaning that the program diverges and goes into an infinite loop that produces effects not visible to the observer at @z@. % {\small\[\begin{array}{cr} \Rule{R-Strong2} {@e1 \evalw@ & @e2 \evalw@} {@e1 ~~z e2 : t!q@} \\\\ \Rule{R-Weak3} {@e1\evalw@} {@e1 ~~z e2 : t!q@} \\\\ \Rule{R-Weak4} {@e2 \evalw@} {@e1 ~~z e2 : t!q@} \end{array}\]} % Since our language with fixpoints are no longer normalizing, the rules R-Term in Sect.~\ref{sec:label} and R-Exp in Sect.~\ref{sec:effect} are not well-founded. Instead, we interpret them coinductively and treat @~~z@ as the largest relation satisfying those rules. \begin{thm}[Noninterference with fixpoints] \ \begin{enumerate} \item Strong noninterference for terms: Theorem~\ref{thm:ni} with R-Strong1 \item Strong noninterference for expressions: Theorem~\ref{thm:niexp} with R-Strong2 \item Weak noninterference for terms: Theorem~\ref{thm:ni} with P-Weak, R-Weak1 and R-Weak2 \item Weak noninterference for expressions: Theorem~\ref{thm:niexp} with P-Weak, R-Weak3 and R-Weak4 \end{enumerate} \end{thm} \begin{comment}[Proof sketch] The idea is to strengthen the coinductive hypothesis by defining another equivalence @~~.z@ that satisfies the same set of rules defined above but also relates diverging terms and is closed under related substitutions of closed values. Since @~~z@ is the largest relation satisfying these equivalence rules by definition, and @~~.z \zspace\supseteq\zspace ~~z@ by construction, it follows that @~~.z \zspace=\zspace ~~z@. This proof is similar to bisimulation proofs in process calculi but our language here is deterministic. The key step is finding the appropriate strengthening of related substitutions; for instance we must relate term fixpoints as follows (and similarly for expression fixpoints): % {\small\[\begin{array}{cr} \Rulez{R-Sub} {@r1 ~.z r2 : g@} {@r1,x|->r1(fix fun x:t.m) ~.z r2,x|->r2(fix fun x:t.m) : g,x:t@} \end{array}\]}% % \end{comment} \fi \section{Decentralized label calculus} \label{sec:dlm} Having established the security property of our core calculus, we now investigate how to make the policy sublanguage more expressive. The key challenge is to extend the policy language in a modular way, reusing the type machinery from the core as much as possible. This section shows how the decentralized label model by Myers and Liskov~\cite{myers97sosp} can be integrated into our core label calculus. Decentralized labels allow different {\em principals} to individually specify fine-grained security policies such as {\em confidentiality} and {\em integrity}. Combined with {\em singleton types}, this extended calculus draws a connection between compile-time dependency analyses and the run-time infrastructure. The benefit is twofold: (1) security policies can now be specified in term of information not known until execution, such as run-time user identities or file access permissions; (2) certificates can be used to regulate declassification and to justify a conditioned version of the noninterference theorem. \subsection{Confidentiality and integrity} \label{sec:confi} Confidentiality policies specify which principals allow which other principals to {\em read} some data, while integrity policies specify which principals {\em trust} some data~\cite{li03fast}. These policy constructors, or {\em label constructors}, provide a finer-grained control of security specification than the {\em label constants} introduced in Sect.~\ref{sec:label}. To model these policies, we treat principals @p@ as abstract types and treat principal delegation @p1<:p2@ as subtyping. That is, @p1@ is a subtype of @p2@ whenever @p1@ {\em delegates to} @p2@ (or, @p2@ is {\em acting for} @p1@). We also introduce two new label constructors, @R@ (read) and @T@ (trust), for confidentiality and integrity: % {\small\[\begin{array}{rcl\@{\qquad}rcl} @l@ &::=& @.. | R p p | T p | l&l | l##l@ & @oo@ &::=& @.. | R o+ o+ | T o- | o+&o+ | o+##o+@ \end{array}\]}% % A label @R p1 p2@ specifies the policy that a data is owned by @p1@ and that @p1@ allows @p2@ to read the data, while a label @T p@ specifies that the data is trusted by @p@. Moreover, we add intersection @l&l@ and union types @l##l@~\cite{barbanera95ic} to precisely model policy sets. Since labels @l@ and principals @p@ are in the same syntactic class, these two constructors can also model principal groups as @p&p@ and @p##p@. Intersection and union types in this paper are used only for labels, principals, and privileges, but not for ordinary types; hence, our language does not have introduction or elimination terms for intersections and unions. This decision helps keeping the static and the dynamic semantics of our language simple. We need both intersection and union types because the two label constructors have different subtyping polarities: @R@ is covariant, while @T@ is contravariant. Having both intersections and unions gives a natural interpretation of principal sets: % {\small\[\begin{array}{rcl} @R [[p1,p2,..,p_n]] p@ &=& @R (p1&p2&..&p_n) p@ \\ @R p [[p1,p2,..,p_n]]@ &=& @R p (p1&p2&..&p_n)@ \\ @T [[p1,p2,..,p_n]]@ &=& @T (p1##p2##..##p_n)@ \end{array}\]}% % \begin{eg} The data \quad@true [R p1 [[p2,p3]]][T [[p1,p2]]]@\quad has two security policies. The first one is a confidentiality policy saying that the data is owned by @p1@, and that @p1@ allows @p2@ and @p3@ to read the data. The second one is an integrity policy saying that both @p1@ and @p2@ trust the data. \qed \end{eg} A decentralized label looks like @[p1: p2, p3;\ p2: p3\ !\ p1,p2]@ traditionally~\cite{myers97sosp,tse04sp}, compared to our notation @[R p1 [[p2,p3]]][R p2 p3][T [[p1 p2]]]@ here. Ours is slightly more verbose but its semantics can be specified more easily in terms of subtyping. In addition, new policy constructors can be added in a uniform way by simply specifying their subtyping polarities. \ifjournal Our constructors @R@ and @T@ could be factored further with the idea of owned policies~\cite{chen04csfw}. For example, we can write @R p1 p2 = O p1 (dcls p2)@ and @T p = O p endr@, where @dcls@ and @endr@ are privileges for confidentiality and integrity (explained in the next subsection). The notation @O p\ \_\ @ means that the principal owns the policy. This ownership notation highlights the authority in a policy and simplifies the downgrading rule; however, it does not generalize to principal delegation and thus we prefer the simpler notation of @R@ and @T@. \fi \subsection{Downgrading as subtyping} \label{sec:auth} The rest of the section discusses various downgrading mechanisms that intentionally leak information~\cite{zdancewic02thesis}. These mechanisms include: \begin{enumerate} \item {\em declassifying} some data to a lower label, \item a principal {\em delegating} to other principals, \item a principal {\em declassifying} some data to other principals for reading, and \item a principal {\em endorsing} the integrity of some data. \end{enumerate} The decentralized label model is essential in the last three mechanisms because each concerns a particular {\em principal}. In Sect.~\ref{sec:cert} we will see how a public key, which represents the concerned principal, can be used to verify a digital certificate, which represents the authority for downgrading. The innovation here is to model downgrading as subtyping. The motivation is that downgrading can be made {\em implicit} through the subsumption rule of subtyping, if the concerned principal {\em explicitly} introduces the authority into the context. This contrasts with the usual approach~\cite{myers97sosp} that uses coercion constructs like @declassify_p m@ and @endorse_p m@ for declassification and endorsement. Both approaches ensure that the authority of the concerned principal is granted before declassification. Our implicit approach, however, allows a simple formulation of certificate-based declassification (to be shown in Sect.~\ref{sec:cert}). Foremost, we extend the type context @d@ to maintain authority, which is a set of authorizations of the form @p<#j@ (a principal @p@ {\em granting} some privilege @j@): % {\small\[\begin{array}{rcl\@{\qquad}rcl} @d@ &::=& @.. | d,p<#j@ \\ @j@ &::=& @.. | del p | dcls p | endr@ & @oo@ &::=& @.. | del o+ | dcls o+ | o+ mod o- <# o+@ \\ @t@ &::=& @.. | t mod p <# j@ & @m@ &::=& @.. | grant p<#j in m | pass x=m in m@ \end{array}\]}% % The three predefined privileges are delegation (@del p@), declassification (@dcls p@), and endorsement (@endr@), corresponding to downgrading for principal subtyping, confidentiality and integrity, respectively. Now, the downgrading mechanisms can be concisely expressed using these additional subtyping rules: {\small\[\begin{array}{c\@{\qquad\qquad}c\@{\qquad\qquad}c} \Rulez{S-Del}{@d |- p1 <# del p2@}{@d |- p1 <: p2@} & \Rulez{S-Read'} {@d |- p1 <# dcls p@}{@d |- R p1 p2 <: R p1 [[p2,p]]@} & \Rulez{S-Trust'}{@d |- p <# endr@}{@d |- T p1 <: T [[p1,p]]@} \end{array}\]}% {\em Authority types} @t mod p <# j@ track the {\em effects} of declassification on the lattice so that later theorems can be stated in terms of the authority: % {\small\[\begin{array}{cc} \Rulez{T-Grant} {@d,p<#j; g |- m : t@ & @d |- p :: \kindp@ & @d |- j :: \kindj@} {@d;g |- grant p<#j in m : t mod p<#j@} & \Rulez{T-Pass} {\begin{array}{ll} @d;g |- m1 : t1 mod p<#j@ \\ @d,p<#j; g,x:t1 |- m2 : t2@ \end{array}} {@d;g |- pass x=m1 in m2 : t2 mod p<#j@} \\\\ @v ::= .. | grant p<#j in v@ & @E ::= .. | grant p<#j in E | pass x=E in e@ \\[1ex] @pass x=(grant p<#j in v) in m --> grant p<#j in m[v/x]@ \hskip-50ex \end{array}\]}% These rules are very close to the typing and evaluation rules for standard monadic types, except that the type context @d@ is now extended with @p<#j@. The value @v@ in the term @grant p<#j in v@ may capture the constraint @p<#j@, and hence, to ensure type preservation, @grant p<#j in v@ is regarded together as a value. As a pleasant bonus of monadic analysis, checking the {\em robustness condition} of downgrading reduces to adding one condition in the label protection rule @d |- l << t@ in Sect.~\ref{sec:label}. In particular, robust declassification says that the program context of a declassification operation should be trusted by the owner of the data~\cite{zdancewic02thesis}. The following rule generalizes the robustness condition to any downgrading mechanism. The intuition is that, for robust downgrading, when @p2@ authorizes some privilege @j@, the program context should have trust (@T p1@) higher than @p2@'s trust (@T p2@). That is @d |- T p2 <: T p1@, or equivalently, @d |- p1 <: p2@. % {\small\[\begin{array}{c} \Rulez{P-Auth} {@d |- T p1 << t@ & @d |- p1 <: p2@} {@d |- T p1 << (t mod p2 <# j)@} \end{array}\]}% % It is known that noninterference does not hold in the presence of downgrading~\cite{myers03jc}. Yet, it is intuitive that if the program does not use any downgrading, the program should still be secure. In fact, a slightly stronger statement holds: if no one transitively downgrades to the observer, the program is still secure. The following modified theorem of noninterference formally captures such intuition. We write @d = d_a,d_{<#}@ to separate the bindings and the authority, and we write @t => t0 mod d@ to collect all required authority in the value positions of the type. For example, @p1,j,p1<#j,p2 |- m : bool -> (bool mod p1 <# j)@ has @d_a=p1,j,p2@ and @d_{<#}=p1<#j@ and @bool -> (bool mod p1 <# j) => (bool -> bool) mod p1 <# j@. These straight-forward rules are defined in our technical report~\cite{tse04esop-tr}. \begin{thm}[Conditioned noninterference]\label{thm:cni} Suppose @d;g |- m : t@, where @d=d_a,d_{<#}@ and @t => t0 mod d0@, and @w |= d_a@ and @r1 ~z r2 : w(g)@. If @d,d0 \not|- p <: z@ for all @p\in dom(d_a)@ such that @d \not|- p <: z@, then @w r1(m) ~~z w r2(m) : w(t)@. \end{thm} \begin{proof} By induction on the typing derivation. Case @fun x:t1.m@: We are given @d;g |- fun x:t1.m : t1 -> t2@. By inversion, we have @d;g,x:t1 |- m : t2@ (*1). Since downgrading in the input propagates to the output in a function, we have @t2 => t3 mod d0@ (*2) for the same @d0@ as in @t1->t2 => t0 mod d0@. Assume @v3 ~z v4 : w(t1)@. We then extend the term substitutions as % {\small\[\begin{array}{rcl\@{\qquad\qquad}rcl} @r1'@ &=& @r1,x|->v3@ & @r2'@ &=& @r2,x|->v4@ \end{array}\]}% % such that @r1' ~z r2' : w(g,x:t1)@ (*3). By induction hypothesis with (*1,*2,*3), {\small\[ @w r1'(m) ~~z w r2'(m) : w(t2)@ \]}% which, by R-Term, @w r1(m)[v3/x] ~~z w r2(m)[v4/x] : w(t2)@. By R-Term again, {\small\[ @w r1(fun x:t.m) v3 ~~z w r2(fun x:t.m) v4 : w(t2)@ \]}% Hence, by R-Fun, @w r1(fun x:t.m) ~~z w r2(fun x:t.m) : w(t1 -> t2)@.\qed \end{proof} The proof is surprisingly similar to that for standard noninterference, showing that this conditioned version is only a slight generalization. In the next subsection, however, we will show how combining this theorem with ideas from public-key infrastructures justifies certificate-based declassification. \subsection{Public keys and certificates} \label{sec:cert} Public-key infrastructures provide public keys and digital certificates for distributed access control. Our motivation here is to connect the type system with the security infrastructure such that a certificate of authority, when verified with a principal's public key, can justify the information leaks due to downgrading. Certificates are also important for auditing purpose. In our previous work~\cite{tse04sp}, we presented the language $\lambda_{\text{RP}}$ for specifying security policies with run-time principals. The type system uses {\em singleton types} to represent run-time principals and an abstract type to represent certificates. Effectively, $\lambda_{\text{RP}}$ models public keys and certificate verifications of public-key infrastructures in a sound type system. Allowing such run-time principals gives programmers more flexibility in specifying security policies. Together with universal and existential quantification, programs can determine the run-time user identity of the system (@getuid@) and write functions polymorphic in principals (@getenv@). Here the type @top_{\kindp}@ represents the top principal, and @' a@ is a singleton type to be explained below. % {\small\[\begin{array}{r\@{\quad}c\@{\quad}l} @getuid@ &:& @() -> some a<:top_{\kindp}. ' a@ \\ @getenv@ &:& @all a<:top_{\kindp}. ' a -> string[R a a]@ \end{array}\]} Our language readily generalizes the idea of {\em run-time types} to run-time labels and run-time privileges as well. For example, access permissions from the file system (@fstat@) can be used as run-time labels to constrain the information flow of data read from a file. Let us recap our previous work on run-time principals~\cite{tse04sp}: % {\small\[\begin{array}{rcl\@{\qquad}rcl} @t@ &::=& @.. | 'p | 'j | cert @ & @m@ &::=& @.. | 'p | 'j | 'p sign 'j | if (m => m <# m) m m@ \end{array}\]}% % The term @'p@ is the run-time representation of principal @p@ and has the singleton type @'p@, carrying the most precise information about the term in the type system. Similarly, @'j@ is the run-time representation of privilege @j@. The term @'p sign 'j@ represents the authority of principal @p@ granting privilege @j@. Such term has the abstract type @cert@ that does not reveal any information at all at the type level. The reason is that we do not trust the validity of the certificate unless verified with the term @if (m1 => m2 <# m3) m4 m5@. More formally: % {\small\[\begin{array}{c} \Axiomz{T-Sin}{@d;g |- 'p : 'p@} \qquad\Axiomz{T-Sin}{@d;g |- 'j : 'j@} \qquad\Axiomz{T-Cert}{@d;g |- 'p sign 'j : cert@} \\\\ \Rulez{T-If} {@d; g |- m1 : cert@ & @d; g |- m2 : 'p@ & @d; g |- m3 : 'j@ & @d,p<#j; g |- m4 : t@ & @d; g |- m5 : t@} {@d; g |- if (m1 => m2 <# m3) m4 m5 : t mod p <# j@} \\\\ \Rulez{E-If1} {@|- 'p1 sign 'j1 => 'p2 <# 'j2@} {@if ('p1 sign 'j1 => 'p2 <# 'j2) m1 m2 --> grant p2 <# j2 in m1@} \end{array}\]}% % The judgment @|- 'p1 sign 'j1 => 'p2 <# 'j2@ defines an external verification procedure of the authority with respect to the principal and the privilege. If the procedure fails, the term @if ('p1 sign 'j1 => 'p2 <# 'j2) m1 m2@ steps to @m2@. There exists a direct mapping from the language constructs (@'p@, @'p sign 'j@, and @|- 'p1 sign 'j1 => 'p2 <# 'j2@\label{judge:ver}) to the mechanisms of public-key infrastructures (public keys and digital certificates). In fact, public-key infrastructures are just one possible implementation that supports distributed access control~\cite{chothia03csfw}. Our previous work~\cite{tse04sp} carries out the design and the proof in an abstract setting and provides constructs for testing delegation and acquiring certificates. We conclude the development of our language by presenting a modified theorem of noninterference. It states that any information leaked by a well-typed program can be justified by certificates in the environment. In fact, the theorem is simply the contrapositive of the conditioned noninterference in Sect.~\ref{sec:auth}. Our technical report~\cite{tse04esop-tr} contains detailed proofs of the type-safety and the following theorem for the full language. \begin{thm}[Certified noninterference] Suppose @d;g |- m : t@, where @d=d_a,d_{<#}@ and @t => t0 mod d0@, and @w |= d_a@ and @r1 ~z r2 : w(g)@. If @w r1(m) \not~~z w r2(m) : w(t)@, then @t=t0 mod d0@ and @d,d0 |- p <: z@ for some @p@ that satisfies @d \not|- p <: z@. \end{thm} \begin{proof} By Theorem~\ref{thm:cni}, extended with singletons and certificates. \end{proof} \ifjournal \begin{figure*}[ht]\small \[\begin{array}{rcl} @d@ &=& @alice,atm,bank,prt,deposit,withdraw [todo give kinding]@ \\[2ex] @login@ &:& @<> -> [R atm atm]@ \\ @request@ &:& @all agent,user.<'agent,'user,cert,cert>[R bank bank]@ \\ && @\qquad -> int[R agent agent, T agent] ! [[agent,bank]]@ \\ @listen@ &:& @<> -> (some agent,user. <'agent,'user,cert,cert,(int[R agent agent] -> <>![[agent,bank]])>)@ \\ && @\qquad [R bank bank, T bank]!agent@ \\ @print@ &:& @int[R atm prt] -> <>@ \\ @get@ &:& @all user. 'user -> int[R [[user,bank]] bank]@ \\ @set@ &:& @all user. 'user -> int[R [[user,bank]] bank] -> <>@ \end{array}\] \bigskip \begin{minipage}[t]{3.4in} @@ return @@ if (acquire 'atm <# \nprime(dcls bank)) @@ => 'atm <# \nprime(dcls bank) then @@ bind x = login <> in @@ let = x in @@ open (user,userid) = y in @@ let creq = acquire userid <# withdraw in @@ let msg = <'atm, userid, cdel, creq> in @@ (run result = request [[atm,user]] msg in @@ return bind balance = result in @@ if (acquire 'atm <# \nprime(dcls prt)) @@ => 'atm <# \nprime(dcls prt) then @@ print balance @@ else <>) ! [[atm,bank]] @@ else error\ "insecure network"@ \end{minipage} \begin{minipage}[t]{3.5in} @@ run result = listen <> in @@ return bind x0 = result, x=x0 in @@ open (agent,user,y) = x in @@ if (acquire 'bank <# \nprime(dcls user)) @@ => 'bank <# \nprime(dcls user) then @@ let = y in @@ if cdel => userid <# 'agent then @@ if creq => userid <# 'withdraw then @@ let old = get [[user]] userid in @@ let balance = bind x = old in x - 100 in @@ let y = set [[user]] userid balance in @@ (run u = reply balance in return <>) ! [[agent,bank]] @@ else <> @@ else error\ "insecure atm" @@ else error\ "insecure network" \end{minipage} \caption{A distributed banking example: ATM's code (left) and bank's code (right)} \label{fig:bank} \end{figure*} \subsection{Implementation and proofs} \label{sec:proof} We have written a prototype interpreter for our full language in OCaml~\cite{ocaml}. Figure~\ref{fig:bank} shows a distributed banking example, which is taken from our previous work~\cite{tse04sp} but rewritten with monadic labels and effects and type-checked with the interpreter. The example models the banking service of requesting money withdraw from the customer's account over a secure network. The action involves four principals: a bank customer @alice@, an ATM machine @atm@, the bank @bank@, and the printer terminal @prt@. Abstract privileges like @deposit@ and @withdraw@ represents different banking services. We are using a construct which is explained in our previous work~\cite{tse04sp} but not here: @acquire m1 <# m2@ where @m1@ represents a run-time principal and @m2@ represents a run-time privilege. The construct models different ways of certification acquisitions such as preinstalled certificates, system calls, or even prompting users at the terminal. The ATM's code starts by checking the security of the network. We use the certificate @'atm <# \nprime(dcls bank)@ to represent the trust of the ATM on the network such that the ATM allows declassification to the bank. Then, the customer @alice@ enters the bank card and types in the password to login the system, revealing her own identity (@userid@) and delegating to the ATM for bank services (@cdel@). After that, the customer selects the service of withdrawing money from the terminal menu and the ATM packs the request message to the bank with its own identity, the customer's identity, the delegation certificate, and the request certificate. After the withdrawal, the ATM prompts if the customer wants to declassify her own balance to the printer terminal. On the server's side, the bank checks the certificates to validate the delegation and the request. The bank can potentially store these certificates for auditing purposes later. The function @listen@ also returns an authenticated channel @reply@ for the bank to send the account balance back to the ATM. For brevity, we model only the side effects of network transmission, where @atm@ and @bank@ can leak information simply by sending to or receive from the network. Besides the interpreter and examples, we also have the proofs for the type-safety theorem and the corresponding noninterference theorems for the full language \iftechreport in the appendix \else in the technical report~\cite{tse04esop-tr}. \fi Currently, we are formalizing our language and the type-safety proof in a logical framework called Twelf~\cite{twelf}. We bypass the higher-order abstract syntax of Twelf and encode variables using de Bruijn index. Doing this gives us the control over the environment and the substitutions so that the typing and evaluation are closely matched with the presentation here. We have also developed a tool to visualize typing rules in Twelf as inference rules and theorem proofs in Twelf as proof derivation trees for reasoning of proof cases. One exciting future work is to prove noninterference in the logical framework; however, it seems that logical relations cannot be directly represented in Twelf~\cite{abel04lfm}. We are writing larger examples in our language interpreter to gain more experience of monadic secure programming. Formalizing the full language semantics and security theorems in a logical framework is also one of our long-term goals of building a rigid foundation for security languages. \fi \section{Related work} \label{sec:relate} The survey by Sabelfeld and Myers~\cite{myers03jc} on language-based information-flow security is an excellent introduction to the field. In particular, their paper cites a long line of research~\cite{myers97sosp,pottier02popl,banerjee02csfw} that studies the interactions of security policies and language features in Java and ML. This paper instead focuses on a smaller set of interesting features with a modular design and with the goal of justifying declassification with certificates. Compared to our previous work~\cite{tse04sp}, this paper concisely expresses the decentralized label model in the polymorphic lambda calculus with subtyping (@F_{<:}@). Various downgrading mechanisms are understood as subtyping such that not only type-safety but also a conditioned version of noninterference can be formulated and proved. We also extensively employ monadic constructs ~\cite{moggi89lics,abadi99popl,crary04fcs} to keep the design and the proofs modular. As a future work, one may check if these constructs satisfy some formal monad laws. Chothia et al.~also use public-key infrastructures to model typed cryptographic operations for distributed access control~\cite{chothia03csfw}. Strecker~\cite{strecker03tr} formalizes an analysis of information flow for $\mu$-Java and proves noninterference in Isabelle by shallow embedding, while Naumann~\cite{naumann04tr} similarly formalizes a core subset of Java in PVS by deep embedding. Our ongoing work has the same goal of proving noninterference in a machine-checkable way. It is known that standard noninterference does not hold in the presence of declassification~\cite{myers03jc}. Hence, it has been a challenging problem to formulate and prove {\em any} variant of noninterference with declassification. Various ideas such as \textit{selective declassification}~\cite{pottier02popl}, {\em delimited release}~\cite{sabelfeld03ss}, and {\em relaxed noninterference}~\cite{li05popl} are proposed to allow downgrading that can be externally justified. \section{Conclusion} \label{sec:con} We have presented the design of a safe and secure information-flow type system with bounded quantification and effects in a monadic style. One of our design decisions is to treat labels, principals and privileges uniformly, as they are all abstract types necessary only for compile-time analyses. This treatment allows reuse of type machinery such as polymorphism, subtyping, and singleton types, keeping the calculus consistent yet general. The integration of the decentralized label model with type constructors allows programmers specify expressive policies, while the use of subtyping to model delegation, declassification, and endorsement simplifies the semantics of downgrading. More importantly, these simplifications lead to a conditioned version of the noninterference theorem that justifies certificate-based downgrading. Formalizing the full language semantics and security theorems is our long-term goal of building a rigid foundation for security-typed languages. One exciting future work is to use Twelf (a logical framework) to mechanically formalize and check the various noninterference theorems presented in this paper. We are also writing larger examples in our language interpreter to gain more experience of monadic secure programming. \section*{Acknowledgments} The authors thank Peng Li, Nitin Khandelwal, Eijiro Sumii, and the anonymous reviewers for their comments on drafts of this paper. This research was supported in part by NSF grant CCR-0311204 \textit{(Dynamic Security Policies)} and NSF grant CNS-0346939 \textit{(CAREER: Language-based Distributed System Security)}. \bibliographystyle{plain} \bibliography{all} \ifjournal \appendix \iftechreport \onecolumn \tableofcontents \bigskip This appendix contains the full syntax, semantics and proofs of the language. Except the logical equivalence and noninterference theorem in Appendix~\ref{sec:ni}, all rules and proofs are mechanically generated by its formalization @apollo.elf@ in Twelf, using the utility \verb|lf2tex| (see \url{http://www.cis.upenn.edu/~stse/lf2tex}). The formalization is not complete: variable operations are abstract, no proofs for substitutions, function totalities, inversions, or canonical forms; yet it should still serves as a good outline to the full proof. There are two \textit{special} lemmas in the mechanical proof that should be mentioned: @psst@ and @stinv@ (page~\pageref{hack:psst}). We prefer the declarative style of subtyping and typing rules but still use Twelf to do \textit{mode checking} for all rules except the subsumption rule for terms (\verb|tyx-sub| on page~\pageref{hack:tyx-sub}). Hence we need to externally justify the use of subsumption with @psst@ (page~\pageref{hack:psst})in the preservation proof \verb|ps-if5| (page~\pageref{hack:ps-if5}). The other special lemma @stinv@ is asserting that the canonical form of the typing derivation for @run x=(return v)!q in m@ involves the use the subsumption for expressions for terms (\verb|tyx-sub| on page~\pageref{hack:etyx-sub}). We need such inversion of subtyping in the preservation proof \verb|eps-run3| on page~\pageref{hack:eps-run3}. \newcommand{\Head}[1]{\newpage\multicolumn{2}{l} {\addtocounter{section}{1} \addcontentsline{toc}{section}{\protect\numberline{\thesection} #1} \setcounter{subsection}{0}\Large\bfseries\thesection\quad{#1}}} \newcommand{\Subhead}[1]{\multicolumn{2}{l} {\addtocounter{subsection}{1} \addcontentsline{toc}{subsection}{\protect\numberline{\thesubsection} #1} \large\bfseries\thesubsection\quad #1}} \newcommand{\Step}[3]{\mbox{\infer[\text{#1}]{#2}{#3}}} \newcommand{\Use}[2]{\mbox{\infer*{#1}{#2}}} \newcommand{\invert}{$\downarrow$} \newcommand{\zpred}[2]{@#1-1 = #2@} \newcommand{\zlt}[2]{@#1 \lt #2@} \newcommand{\zge}[2]{@#1 \ge #2@} \newcommand{\zne}[2]{@#1 \ne #2@} \newcommand{\zltge}[2]{@#1 \diamond #2@} \newcommand{\zvenve}[4]{@|-^? \nprime #1 sign \nprime #2 => \nprime #3 <# \nprime#4@} \newcommand{\zltgex}[1]{#1} \newcommand{\zxz}[0]{@x@} \newcommand{\zz}[0]{@0@} \newcommand{\zs}[1]{@#1+1@} \newcommand{\zkt}[0]{@T@} \newcommand{\zkl}[0]{@L@} \newcommand{\zkp}[0]{@P@} \newcommand{\zkj}[0]{@J@} \newcommand{\zkpj}[0]{@PJ@} \newcommand{\zg}[0]{@g@} \newcommand{\zk}[0]{@k@} \newcommand{\zd}[0]{@d@} \newcommand{\zdn}[0]{@empty@} \newcommand{\zu}[0]{@u@} \newcommand{\zh}[0]{@h@} \newcommand{\ze}[0]{@e@} \newcommand{\zm}[0]{@m@} \newcommand{\zt}[0]{@t@} \newcommand{\zq}[0]{@q@} \newcommand{\zp}[0]{@p@} \newcommand{\zj}[0]{@j@} \newcommand{\zl}[0]{@l@} \newcommand{\zn}[0]{@n@} \newcommand{\zx}[0]{@x@} \newcommand{\zvar}[1]{@#1@} \newcommand{\zevar}[1]{@#1@} \newcommand{\zgn}[0]{@\cdot@} \newcommand{\zhn}[0]{@\cdot@} \newcommand{\zgt}[2]{@#1,x:#2@} \newcommand{\zgq}[3]{@#1,x:#2!#3@} \newcommand{\ztauth}[3]{@#1 mod\ #2 <# #3@} \newcommand{\zdt}[2]{@#1,a<:#2@} \newcommand{\zdp}[3]{@#1,#2 <# #3@} \newcommand{\zht}[2]{@#1,a<:#2@} \newcommand{\zhb}[2]{@#1,a<:#2@} \newcommand{\zha}[3]{@#1,#2 #> #3@} \newcommand{\zhl}[3]{@#1,#2 <# #3@} \newcommand{\zhuu}[3]{@#1,#2 <# #3@} \newcommand{\zhu}[2]{@#1,#2@} \newcommand{\zcat}[3]{@#1,#2=#3@} \newcommand{\ztunit}[0]{@<>@} \newcommand{\ztprod}[2]{@< #1,#2 >@} \newcommand{\ztsum}[2]{@#1+#2@} \newcommand{\ztfun}[2]{@#1 -> #2@} %\newcommand{\ztfun}[3]{@#1 -> #2 \zspace!\zspace #3@} \newcommand{\zeff}[2]{@#1 \zspace!\zspace #2@} \newcommand{\zteff}[2]{@#1 \zspace!\zspace #2@} \newcommand{\zret}[1]{@ret\ #1@} \newcommand{\zrun}[2]{@run x=#1 in\ #2@} \newcommand{\zseq}[2]{@seq x=#1 in\ #2@} \newcommand{\zpass}[2]{@pass x=#1 in\ #2@} \newcommand{\zutop}{@top@} \newcommand{\zttop}{@top@} \newcommand{\ztop}{@top@} \newcommand{\ztbot}{@bot@} \newcommand{\ztvar}[1]{@#1@} \newcommand{\zfix}[1]{@fix\ #1@} \newcommand{\zefix}[3]{@fix\ x:#1!#2. #3@} \newcommand{\zlift}[1]{@lift\ #1@} \newcommand{\zuvar}[1]{@#1@} \newcommand{\ztall}[2]{@all a<:#1. #2@} %\newcommand{\ztall}[3]{@all a<:#1. #2 \zspace!\zspace #3@} \newcommand{\ztsome}[2]{@some a<:#1. #2@} %\newcommand{\ztunion}[2]{@#1 \cup #2@} %\newcommand{\ztinter}[2]{@#1 \cap #2@} \newcommand{\ztunion}[2]{@#1 ## #2@} \newcommand{\ztinter}[2]{@#1 & #2@} \newcommand{\ztrep}[1]{@{}^\prime #1@} \newcommand{\ztsin}[1]{@{}^\prime #1@} \newcommand{\ztcert}[0]{@cert@} \newcommand{\ztlab}[2]{@#1 [#2]@} \newcommand{\ztpot}[1]{@#1++@} \newcommand{\ztdel}[1]{@del\ #1@} \newcommand{\ztendr}[0]{@endr@} \newcommand{\ztdcls}[1]{@dcls\ #1@} \newcommand{\ztread}[2]{@R\ #1\ #2@} \newcommand{\zttrust}[1]{@T\ #1@} \newcommand{\zunit}[0]{@<>@} \newcommand{\zfun}[2]{@fun x:#1.#2@} \newcommand{\zapp}[2]{@#1\ #2@} \newcommand{\zprod}[2]{@< #1,#2 >@} \newcommand{\zprl}[1]{@prl\ #1@} \newcommand{\zprr}[1]{@prr\ #1@} \newcommand{\zinl}[2]{@inl\ #1 as\ #2@} \newcommand{\zinr}[2]{@inr\ #1 as\ #2@} %\newcommand{\zcase}[3]{@case\ #1 of\ #2 |\ #3@} \newcommand{\zcase}[3]{@case\ #1\ #2\ #3@} \newcommand{\zpoly}[2]{@poly a<:#1. #2@} \newcommand{\znew}[1]{@new a in\ #1@} \newcommand{\zinst}[2]{@#1 [[#2]]@} \newcommand{\zpack}[3]{@pack\ (#1,#2) as\ #3@} \newcommand{\zopen}[2]{@open\ (a,x) = #1 in\ #2@} \newcommand{\zas}[2]{@#1 as\ #2@} \newcommand{\zrep}[1]{@{}^\prime #1@} \newcommand{\zsin}[1]{@{}^\prime #1@} \newcommand{\zcert}[2]{@\nprime #1\ <# \nprime #2@} \newcommand{\zfram}[2]{@Fram\ (#1,#2)@} \newcommand{\zclos}[2]{@Clos\ (#1,#2)@} %\newcommand{\zeas}[2]{@#1 as\ #2@} \newcommand{\zeas}[2]{@#1@} \newcommand{\zety}[5]{@#1;#2 |- #3 : #4 \zspace!\zspace #5@} \newcommand{\zetyx}[5]{@#1;#2 |- #3 : #4 \zspace!\zspace #5@} \newcommand{\zty}[4]{@#1;#2 |- #3 : #4@} \newcommand{\ztyx}[4]{@#1;#2 |- #3 : #4@} %\newcommand{\zty}[5]{@#1;#2 |- #3 : #4 |\ #5@} %\newcommand{\ztyx}[5]{@#1;#2 |- #3 : #4 |\ #5@} \newcommand{\zgtmem}[3]{@#2 : #3 \in #1@} \newcommand{\zgqmem}[4]{@#2 : #3 ! #4 \in #1@} \newcommand{\zdtmem}[3]{@#2 <: #3 \in #1@} \newcommand{\zdpmem}[3]{@#2 <# #3 \in #1@} \newcommand{\zmap}[2]{@#1[[x]] = #2@} \newcommand{\zmapb}[3]{@#1[[#2]] = #3@} \newcommand{\zmapa}[3]{@#2 #> #3 \in #1@} \newcommand{\zval}[1]{@val\ #1@} \newcommand{\zuval}[1]{@val\ #1@} \newcommand{\zwf}[3]{@#1;#2 |- #3 wf@} \newcommand{\zvarwf}[2]{@#1 |- #2 wf@} \newcommand{\ztwf}[2]{@#1 |- #2 wf@} \newcommand{\ztvarwf}[2]{@#1 |- #2 wf@} \newcommand{\zgdis}[3]{@#1[#2]=#3@} \newcommand{\zhdis}[3]{@#1[#2]=#3@} \newcommand{\zindep}[1]{@x\not\in fv(#1)@} \newcommand{\zgindep}[1]{@a \not\in tfv(#1)@} \newcommand{\ztindep}[1]{@a \not\in tfv(#1)@} \newcommand{\zup}[3]{@\uparrow_{#2} #1 = #3@} \newcommand{\zdown}[3]{@\downarrow_{#2} #1 = #3@} \newcommand{\zetdown}[3]{@\downarrow_{#2} #1 = #3@} \newcommand{\zttdown}[3]{@\downarrow_{#2} #1 = #3@} \newcommand{\zgup}[4]{@\uparrow^{#2}_{#3} #1 = #4@} \newcommand{\zhup}[4]{@\uparrow^{#2}_{#3} #1 = #4@} \newcommand{\zmmsub}[3]{@#1 [#2 / x] = #3@} %\newcommand{\zsubs}[4]{@#1 [#2 / #3] = #4@} %\newcommand{\zev}[3]{@#1 |\ #2 --> #3@} \newcommand{\zev}[2]{@#1 --> #2@} \newcommand{\zeev}[3]{@#1 ==>{#3} #2@} \newcommand{\zeval}[3]{@#1 |\ #2 -->^* #3@} %\newcommand{\zvalev}[2]{@#1 |\ evval\ #2@} \newcommand{\zevval}[1]{@evval\ #1@} \newcommand{\zeevuval}[1]{@evval\ #1@} \newcommand{\zlow}[0]{@L@} \newcommand{\zhigh}[0]{@H@} \newcommand{\zlab}[2]{@#1 [#2]@} \newcommand{\zbind}[2]{@bind\ x=#1 in\ #2@} \newcommand{\zacq}[2]{@acq\ #1 #> #2@} \newcommand{\zif}[5]{@if (#1 => #2 <# #3)\ #4\ #5@} \newcommand{\zve}[4]{@|- \nprime #1 sign \nprime #2 => \nprime #3 <# \nprime#4@} \newcommand{\znve}[4]{@\not|- \nprime #1 sign \nprime #2 => \nprime #3 <# \nprime #4@} \newcommand{\zifcert}[5]{@if (#1 => #2 #> #3)\ #4\ #5@} \newcommand{\zifgrant}[4]{@if (#1 <: #2)\ #3\ #4@} %\newcommand{\zif}[4]{@if (#1 <: #2)\ #3\ #4@} \newcommand{\zlet}[3]{@let\ #1 <# #2\ in\ #3@} \newcommand{\zsl}[2]{@#1 <: #2@} \newcommand{\znsl}[2]{@#1 \not<: #2@} \newcommand{\zplab}[3]{@#1 |- #3 << #2@} \newcommand{\zppot}[2]{@#1 |- \dagger << #2@} \newcommand{\ztup}[3]{@\uparrow_{#2} #1 = #3@} \newcommand{\ztmap}[3]{@#1[[#2]] = #3@} \newcommand{\zttsub}[3]{@#1 [#2 / a] = #3@} \newcommand{\zetsub}[3]{@#1 [#2 / a] = #3@} \newcommand{\zmtsub}[3]{@#1 [#2 / a] = #3@} \newcommand{\zemsub}[3]{@#1 [#2 / x] = #3@} \newcommand{\zeesub}[3]{@#1 [#2 / x] = #3@} \newcommand{\zetindep}[2]{@#2 \not\in ftv (#1)@} \newcommand{\zttindep}[2]{@#2 \not\in ftv (#1)@} \newcommand{\zpm}[3]{@#1 |- #2 \Uparrow #3@} \newcommand{\zst}[3]{@#1 |- #2 <: #3@} \newcommand{\zstx}[3]{@#1 |- #2 <: #3@} \newcommand{\znst}[3]{@#1 \not|- #2 <: #3@} \newcommand{\zkd}[3]{@#1 |- #2 :: #3@} %\newcommand{\zsubq}[3]{@#1 |- #2 <: #3@} \newcommand{\znsub}[3]{@#1 \not|- #2 <: #3@} \newcommand{\zjoin}[4]{@#1 |- #2 \sqcup #3 = #4@} \newcommand{\zmeet}[4]{@#1 |- #2 \sqcap #3 = #4@} \newcommand{\zeqv}[4]{@#1 ~z #2 : #3@} \newcommand{\zeqm}[4]{@#1 ~~z #2 : #3@} \newcommand{\zequ}[4]{@#1 ~z #2 : #3@} \newcommand{\zeqe}[4]{@#1 ~~z #2 : #3@} \newcommand{\zeqvx}[4]{@all (#1 ~z #2 : #3).@} \setlength\LTleft{-25pt} \begin{footnotesize} \begin{longtable}{cr} \csname \@\@input\endcsname apollo.tex2 \end{longtable} \end{footnotesize} \section{Noninterference}\label{sec:ni} \subsection{Logical equivalence for values} \[\begin{array}{cr} \Axiom{R-Unit}{@<> ~z <> : <>@} \\\\ \Rule{R-Prod}{@v1 ~z v3 : t1@ & @v2 ~z v4 : t2@} {@ ~z : @} \\\\ \Rule{R-Inl}{@v1 ~z v2 : t1@} {@inl v1 ~z inl v2 : t1+t2@} \\\\ \Rule{R-Inr}{@v1 ~z v2 : t2@} {@inr v1 ~z inr v2 : t1+t2@} \\\\ \Rule{R-Fun}{@all (v3 ~z v4 : t1). v1 v3 ~~z v2 v4 : t2@}{@v1 ~z v2 : t1 -> t2@} \\\\ \Rule{R-Lab1}{@l <: z@ & @v1 ~z v2 : t@} {@v1[l] ~z v2[l] : t[l]@} \\\\ \Rule{R-Lab2}{@l \not<: z@} {@v1[l] ~z v2[l] : t[l]@} \\\\ \Rule{R-All} {@all (t2 <: t1). v1[[t2]] ~~z v2[[t2]] : t[t2/a]@} {@v1 ~z v2 : all a<:t1. t@} \\\\ \Rule{R-Some} {@v1 ~z v2 : t[t1/a]@} {@pack (t1,v1) as some a<:t2.t ~z pack (t1,v2) as some a<:t2.t : some a<:t2.t@} \\\\ \Rule{R-Eff}{@e1 ~~z e2 : t!q@} {@e1!q ~z e2!q : t!q@} \\\\ \Rule{R-Lift}{@v1 ~z v2 : t@} {@lift v1 ~z lift v2 : t++@} \\\\ \Rule{R-Auth} {@v1 ~z v2 : t@} {@grant p<#j in v1 ~z grant p<#j in v2 : t mod p1<# j2@} \\\\ \Axiom{R-Sin}{@'p ~z 'p : 'p@} \\\\ \Axiom{R-Cert}{@'p1 <# 'p2 ~z 'p1 <# 'p2 : 'p1 <# 'p2@} \\\\ \Rule{R-Ret}{@v1 ~z v2 : t@} {@return v1 ~z return v2 : t!q@} \\\\ \end{array}\] \subsection{Logical equivalence for terms and expressions} \[\begin{array}{cr} \Rule{R-Term}{@m1 -->* v1@ & @m2 -->* v2@ & @v1 ~z v2 : t@} {@m1 ~~z m2 : t@} \\\\ \Rule{R-Exp} {@e1 -=>{n} u1@ & @e2 -=>{n} u2@ & @u1 ~z u2 : t!q@} {@e1 ~~z e2 : t!q@} \\\\ \Rule{R-Strong1}{@m1-->^\omega@ & @m2-->^\omega@} {@m1 ~~z m2 : t@} \\\\ \Rule{R-Weak1}{@m1-->^\omega@} {@m1 ~~z m2 : t@} \\\\ \Rule{R-Weak2}{@m2 -->^\omega@} {@m1 ~~z m2 : t@} \\\\ \Rule{R-Strong2} {@e1 \evalw@ & @e2 \evalw@} {@e1 ~~z e2 : t!q@} \\\\ \Rule{R-Weak3} {@e1\evalw@} {@e1 ~~z e2 : t!q@} \\\\ \Rule{R-Weak4} {@e2 \evalw@} {@e1 ~~z e2 : t!q@} \\\\ \end{array}\] \subsection{Standard noninterference} \begin{thm}[Noninterference] \ \begin{enumerate} \item If @d;g |- m : t@ and @w |= d@ and @r1 ~z r2 : w(g)@, then @w r1(m) ~~z w r2(m) : w(t)@. \item If @d;g |- e : t ! q@ and @w |= d@ and @r1 ~z r2 : w(g)@, then @w r1(e) ~~z w r2(e) : w(t) ! w(q)@. \end{enumerate} \end{thm} \begin{comment} The idea is to strengthen the coinductive hypothesis by defining another equivalence @~~.z@ that satisfies the same set of rules defined above for @~~z@ but also relates diverging terms and is closed under related substitutions of closed values. Since @~~z@ is the largest relation satisfying these equivalence rules by definition, and @~~.z \zspace\supseteq\zspace ~~z@ by construction, it follows that @~~.z \zspace=\zspace ~~z@. This proof is similar to bisimulation proofs in process calculi but our language here is deterministic. Let @m ~~.z m : t@ be the largest relation satisfying the following rules: % {\[\begin{array}{cr} \Rule{RR-Term1}{@m1 ~~z m2 : t@} {@m1 ~~.z m2 : t@} \\\\ \Rule{RR-Term2} {@d;g |- m : t@ & @w |= d@ & @r1 ~~.z r2 : w(g)@} {@w r1(m) ~~.z w r2(m) : w(t)@} \end{array}\]}% % Similarly, let @e ~~.z e : t@ be the largest relation satisfying the following rules: % {\[\begin{array}{cr} \Rule{RR-Exp1}{@e1 ~~z e2 : t ! q@} {@e1 ~~.z e2 : t@} \\\\ \Rule{RR-Exp2} {@d;g |- e : t ! q@ & @w |= d@ & @r1 ~~.z r2 : w(g)@} {@w r1(e) ~~.z w r2(e) : w(t) ! w(q)@} \end{array}\]}% % Also, extend term substitutions @r@ to allow substitutions with terms and expressions, rather than just values: % {\[\begin{array}{rcl} @r@ &::=& @empty | r,x|->m | r,x|->e@ \end{array}\]}% % Then, let @r ~~.z r : g@ be the largest relation satisfying the following rules: % {\[\begin{array}{cr} \Rule{RR-Sub1}{@r1 ~z r2 : g@} {@r1 ~~.z r2 : g@} \\\\ \Rule{RR-Sub2}{@r1 ~~.z r2 : w(g)@} {@r1,x|->w r1(fix fun x:t.m) ~~.z r2,x|->w r2(fix fun x:t.m) : w(g,x:t)@} \\\\ \Rule{RR-Sub3}{@r1 ~~.z r2 : w(g)@} {@r1,x|->w r1(fix x:t!q.e) ~~.z r2,x|->w r2(fix x:t!q.e) : w(g,x:t!q)@} \end{array}\]}% % We claim without proving that the equivalence rules above (R-Weak* and R-Strong*) for terms and expressions are the same as the following rules: \[\begin{array}{cr} \Rule{RR-Strong1}{@m1 -->+ m3@ & @m2 -->+ m4@ & @m3 ~~z m4: t@} {@m1 ~~z m2 : t@} \\\\ \Rule{RR-Strong2}{@e1 -=> e3@ & @e2 -=> e4@ & @e3 ~~z e4 : t@} {@e1 ~~z e2 : t@} \\\\ \Rule{RR-Weak1}{@m1 --> m3@ & @m2 -->* m4@ & @m3 ~~z m4: t@} {@m1 ~~z m2 : t@} \\\\ \Rule{RR-Weak2}{@m1 -->* m3@ & @m2 --> m4@ & @m3 ~~z m4: t@} {@m1 ~~z m2 : t@} \\\\ \Rule{RR-Values1}{@v1 ~z v2 : t@}{@v1 ~~z v2 : t@} \\\\ \Rule{RR-Values2}{@u1 ~z u2 : t@}{@u1 ~~z u2 : t@} \\\\ \end{array}\] Now, after setting up all these auxiliary definitions, we are ready to prove that @~~.z@ also satisfies the RR-* rules above. If the two terms are related by RR-Term1 or two expressions are related by RR-Exp1, then the case is trivial. Assume that we are in the case of RR-Term2 or RR-Exp2. By inversion of RR-Term2, we have @d;g |- m : t@ and @w |= d@ and @r1 ~~.z r2 : w(g)@. By inversion of RR-Exp2, we have @d;g |- e : t ! q@ and @w |= d@ and @r1 ~~.z r2 : w(g)@. We proceed to complete the proof by mutual induction on @g |- e : t@ and @g |- m : t@. We omit the cases for unit, sums and products, which are straight-forwarded. The proof here is for strong noninterference (no P-Weak), but can readily be generalized to handle weak noninterference. The cases for T-Bind, T-Ret and T-Run without fixpoints are shown in the main text of this paper; the proof for those cases with RR-* rules can be adapted by case analysis on their evaluations. The cases for T-Grant, T-Pass and T-If are handled only in the condition version of noninterference (see next subsection). \begin{itemize} \item T-Var: if @r1 ~~.z r2 : g@ by RR-Sub1, then @r1(x) ~z r2(x) : t@ by the definition of @r ~z r : g@. Assume that we are in the case of RR-Sub2 and @r1(x) = w r1(fix fun x:t.m)@ and @r2(x) = w r2(fix fun x:t.m)@. Because @r(x) = w r1(fix fun x:t.m)@ and thus @(r1,x|->w r1(fix fun x:t. m))=r1@, we have % {\[\begin{array}{cl} & @w r1(fix fun x:t.m)@ \\ @=@ & @fix fun x:t. w r1 (m)@ \\ @-->@ & @w r1(m)[fix fun x:t. w r1(m) / x]@ \\ @=@ & @w r1(m)[w r1(fix fun x:t. m) / x]@ \\ @=@ & @w (r1,x|->w r1(fix fun x:t. m))(m)@ \\ @=@ & @w r1(m)@ \\ \end{array}\]}% % Similarly, @w r2(fix fun x:t.m)=w r2(m)@. Hence, by RR-Strong1 and RR-Term2, we conclude that @w r1(x) ~~.z w r2(x) : w(t)@. The case for expressions with RR-Sub3 and RR-Strong2 is similar. \item T-Fix: By inversion, we have @d;g |- m : t -> t@. By progress theorem, either @w r1(m)@ takes a step (@w r1(m) --> m1@), or @w r1(m)@ is a value (@w r1(m)=v1@), which has the canonical form @w r1(m)=fun x:t. m1@. Again, by progress theorem, either @w r2(m)@ takes a step (@w r2(m) --> m2@) or @w r2(m)@ is a value (@w r2(m)=v@), which has the canonical form @w r1(m)=fun x:t. m2@. By RR-Term2, we have @w r1(m) ~~.z w r2(m) : w(t -> t)@. If @w r1(fix m)@ and @w r2(fix m)@ take steps, we have @w r1(fix m) ~~.z w r1(fix m) : w(t)@ by RR-Strong1. Otherwise, % {\[\begin{array}{rcl} @w r1(fix (fun x:t. m))@ &@-->@& @w r1(m)[w r1(fix (fun x:t. m))/x] = w r1(m)@ \\ \end{array}\]}% % in which case the reasoning is similar to the case for T-Var. Hence, by RR-Strong1 and RR-Term2, we conclude that @w r1(fix m) ~~.z r2(fix m) : w(t)@. The case for expressions with RR-Strong2 is similar. \item T-Poly: By inversion, we have @d,a<:t1; g |- m:t2@. Assume @t <: t1@ and then extend @w0 = w, a |-> t@ such that @w0 |= d,a<:t1@. Since @r1 ~~.z r2 : w(g)@ and @a \not\in ftv(g)@, we have @r1 ~~.z r2 : w0(g)@. By RR-Term2, we have @w0 r1(m) ~~.z w0 r2(m) : w0(t2)@. Note that @w0(t2) = (w,a|->t)(t2) = w(t2[t/a])@. By R-All, we have @w r1(poly a<:t1. m) ~~.z w r2(poly a<:t1. m) : w(all a<:t1. m)@. \item T-Inst: By inversion, we have @d;g |- m : all a<:t1.t2@ and @d |- t3 <: t1@. By RR-Term2, @w r1(m) ~~.z w r2(m) : w(all a<:t1.t2)@. If both @w r1(m)@ and @w r2(m)@ take steps, they are still related by RR-Strong1. Assume both terms are values: @w r1(m)=v1@ and @w r2(m)=v2@. By inversion of R-All, for all @w(t3) <: w(t1)@, we have @v1 [[w(t3)]] ~~.z v2 [[w(t3)]] : w(t2[t3/a])@. Hence, by RR-Strong1, we conclude that @w r1(m [[t3]]) ~~.z w r2(m [[t3]]) : w(t2[t3/a])@. \item T-Pack: By inversion, we have @d;g |- m:t3@. The case when @m@ takes a step is similar to that for T-Fix. Assume @m@ is a value. By RR-Term2, we have @w r1(m) ~~.z w r2(m) : w(t3)@. By R-Some, we have @w r1(pack (t,m) as some a<:t1.t2) ~~.z w r2(pack (t,m) as some a<:t1.t2) : w(some a<:t1.t2)@. \item T-Open: By inversion, we have @d;g |- m1 : some a<:t1.t2@ and @d,a<:t1;g,x:t2 |- m2:t@. By RR-Term2, @w r1(m1) ~~.z w r2(m1) : w(some a<:t1.t2)@. If both @w r1(m)@ and @w r2(m)@ take steps, they are still related by RR-Strong1. Assume both terms are values: @w r1(m1)=pack (t,v1) as some a<:t1.t2@ and @w r2(m1)=pack (t,v2) as some a<:t1.t2@, where @w(t)<:w(t1)@. By inversion of R-Some, we have @v1 ~.z v2 : w(t2[t/a])@. Extend @w0 = w,a|->t@ such that @w0 |= d,a<:t1@. Also, extend @r3 = r1,x|->v1@ and @r4 = r2,x|->v2@ such that @r3 ~~.z r4 : w(g),x:w(t2[t/a])@. Since @a \not\in ftv(g)@, we have @r3 ~~.z r4 : w0(g,x:t2)@. By RR-Term2, @w0 r3(m2) ~~.z w0 r4(m2) : w0(t)@. Since @a \not\in ftv(g)@, we have @w0(t) = w(t)@. Hence, by RR-Strong1, we conclude that @w r1(open (a,x)=m1 in m2) ~~.z w r1(open (a,x)=m1 in m2) : w(t)@. \item T-Eff: by mutual induction hypothesis (RR-Exp2). \item T-Fix: similar to T-Lab. \item T-Lift: similar to T-Lab. \item T-Seq: similar to T-Bind. \item T-Sin: by R-Sin. \item T-Cert: by R-Cert. \end{itemize} \end{comment} \subsection{Authorities for proper types} % {\small\[\begin{array}{cr} \Axiom{M-Unit}{@<> => .@} \\\\ \Rule{M-Prod}{@t1 => d1@ & @t2 => d2@} {@ => d1,d2@} \\\\ \Rule{M-Sum}{@t1 => d1@ & @t2 => d2@} {@t1+t2 => d1,d2@} \\\\ \Rule{M-Fun} {@t2 => t mod d@} {@t1 -> t2 => (t1 -> t) mod d@} \\\\ \Axiom{M-Top}{@top => .@} \\\\ \Axiom{M-Bot}{@bot => .@} \\\\ \Axiom{M-Var}{@a => .@} \\\\ \Rule{M-All} {@t2 => t mod d@} {@all a<:t1.t2 => (all a<:t1.t) mod d@} \\\\ \Rule{M-Some} {@t2 => t mod d@} {@some a<:t1.t2 => (some a<:t1.t) mod d@} \\\\ \Rule{M-Lab}{@t => d@} {@t[l] => d@} \\\\ \Rule{M-Eff}{@t => d@} {@t!q => d@} \\\\ \Rule{M-Pot}{@t => d@} {@t++ => d@} \\\\ \Rule{M-Auth} {@t => t0 mod d@} {@t mod p<#j => d,p<#j@} \\\\ \Axiom{M-Sin}{@'p => .@} \\\\ \Axiom{M-Cert}{@cert => .@} \end{array}\]}% % \newpage \subsection{Conditioned noninterference} \begin{thm}[Conditioned and certified noninterference] \ \begin{enumerate} \item Suppose @d;g |- m : t@, where @d=d_a,d_{<#}@ and @t => t0 mod d0@, and @w |= d_a@ and @r1 ~z r2 : w(g)@. If @d0 \not|- p <: z@ for all @p\in dom(d_a)@ that satisfy @d \not|- p <: z@, then @w r1(m) ~~z w r2(m) : w(t)@. \item Suppose @d;g |- e : t!q@, where @d=d_a,d_{<#}@ and @t => t0 mod d0@, and @w |= d_a@ and @r1 ~z r2 : w(g)@. If @d0 \not|- p <: z@ for all @p\in dom(d_a)@ that satisfy @d \not|- p <: z@, then @w r1(e) ~~z w r2(e) : w(t)!w(q)@. \item Suppose @d;g |- m : t@, where @d=d_a,d_{<#}@ and @t => t0 mod d0@, and @w |= d_a@ and @r1 ~z r2 : w(g)@. If @w r1(m) \not~~z w r2(m) : w(t)@, then @t=t0 mod d0@ and @d0 |- p <: z@ for some @p@ that satisfies @d \not|- p <: z@ \item Suppose @d;g |- e : t ! q@, where @d=d_a,d_{<#}@ and @t => t0 mod d0@, and @w |= d_a@ and @r1 ~z r2 : w(g)@. If @w r1(e) \not~~z w r2(e) : w(t)!w(q)@, then @t=t0 mod d0@ and @d0 |- p <: z@ for some @p@ that satisfies @d \not|- p <: z@ \end{enumerate} \end{thm} \begin{comment} The last two statements are the converse of the first two statements. As shown in the proof for the case T-Fun in Sect.~\ref{sec:auth}, this conditioned version is only a slight generalization of the standard noninterference theorem and the proof goes through almost as before, except for T-Grant. Case T-Grant: given the typing @d;g |- grant p1 <# j2 in m : t mod p1 <# p2@, where @d,p<#j; g |- m : t@. By inversion of M-Auth, @t => d0@ and @t mod p1 <# j2 => d0,p<#j@. Assume @p\in dom(d_a)@ and @d \not|- p <: z@ such that @d0 \not|- p <: z@. By the induction hypothesis, @w r1(m) ~~z w r2(m) : w(t)@. Assume further that @d0,p<#j |- p <: z@. Then, by R-Auth, we can conclude that @w r1(grant p1 <# j2 in m) ~~z w r2(grant p1 <# j2 in m) : w(t mod p<#j)@. \end{comment} \begin{footnotesize} \printindex \end{footnotesize} \else \section{Syntax} {\small\[\begin{array}{lrcl} \text{Type contexts} & @d@ &::=& @empty | a<:t | t<#t@ \\ \text{Term contexts} & @g@ &::=& @empty | x:t | x:t!q@ \\ \\ \text{Kinds} & @k@ &::=& @T | L | P | J@ \\ \text{Labels} & @l@ &\equiv& @t@ \\ \text{Principals} & @p@ &\equiv& @t@ \\ \text{Privileges} & @j@ &\equiv& @t@ \\ \text{Types} & @t@ &::=& @<> | | t+t | t->t | top | bot@ \\ &&& @| a | all a<:t.t | some a<:t.t@ \\ &&& @| l&l | l##l | t[l]@ \\ &&& @| t ! q@ \\ &&& @| t++@ \\ &&& @| R p p | T p@ \\ &&& @| t mod p <# j@ \\ &&& @| 'p | cert@ \\ &&& @| dcls p | endr@ \\ \\ \text{Terms} & @m@ &::=& @<> | | prj1 m | prj2 m@ \\ &&& @| inj1 m | inj2 m | case m m m@ \\ &&& @| x | fun x:t.m | m m@ \\ &&& @| poly a<:t.m | m[[t]]@ \\ &&& @| pack (t,m) as t@ \\ &&& @| open (a,x)=m in m@ \\ &&& @| m[l] | bind x=m in m@ \\ &&& @| e ! q@ \\ &&& @| fix m | lift m@ \\ &&& @| seq x=m in m@ \\ &&& @| grant p<#j in m@ \\ &&& @| pass x=m in m@ \\ &&& @| 'p | 'p sign 'p@ \\ &&& @| if (m => m <# m) m m@ \\ \\ \text{Values} & @v@ &::=& @<> | | inj1 v | inj2 v@ \\ &&& @| fun x:t.m | poly a<:t.m@ \\ &&& @| pack (t,v) as t@ \\ &&& @| v[l]@ \\ &&& @| e ! q@ \\ &&& @| lift v@ \\ &&& @| grant p<#j in v@ \\ &&& @| 'p | 'p sign 'p@ \\ \\ \text{Expressions} & @e@ &::=& @return m | run x=m in e@ \\ &&& @| x | fix x:t!q.e@ \\ \\ \text{Values} & @u@ &::=& @return v@ \end{array}\]} {\small\[\begin{array}{lrcl} \text{Holes} & @E@ &::=& @ | | prj1 E | prj2 E@ \\ &&& @| inj1 E | inj2 E | case E m m@ \\ &&& @| E m | v E@ \\ &&& @| E[[t]] | pack (t,E) as t@ \\ &&& @| open (a,x)=E in m@ \\ &&& @| E[l]@ \\ &&& @| bind x=E in m@ \\ &&& @| fix E | lift E@ \\ &&& @| seq x=E in m@ \\ &&& @| grant p<#j in E@ \\ &&& @| pass x=E in m@ \\ &&& @| if (E => m <# m) m m@ \\ &&& @| if (v => E <# m) m m@ \\ &&& @| if (v => v <# E) m m@ \\ &&& @| return E@ \\ &&& @| run x=E in e@ \\ &&& @| run x=(return E)!q in e@ \\ \\ \text{Polarities} & @oo@ &::=& @ | o+ + o+ | o- -> o+@ \\ &&& @| all a<:o..o+ | some a<:o..o+@ \\ &&& @| o+&o+ | o+##o+ | o+[o+]@ \\ &&& @| o+ ! o-@ \\ &&& @| o+++@ \\ &&& @| R o+ o+ | T o-@ \\ &&& @| o+ mod o- <# o+@ \\ &&& @| \ \nprime o.@ \\ &&& @| dcls o+@ \\ \\ \text{Type subst} & @w@ &::=& @empty | w,a|->t@ \\ \text{Term subst} & @r@ &::=& @empty | r,x|->v | r,x|->u@ \end{array}\]}% % \section{Judgments} {\small\[\begin{array}{llr} \text{Term Typing} & @d;g |- m : t@ & \text{Section~\ref{judge:ty}} \\ \text{Exp typing} & @d;g |- e : t!q@ & \text{Section~\ref{judge:ety}} \\ \text{Subtyping} & @d |- t <: t@ & \text{Section~\ref{judge:sty}}\\ \\ \text{Label Protection} & @d |- l << t@ & \text{Section~\ref{judge:pt}}\\ \text{Pointed Protection} & @d |- \dagger << t@ & \text{Section~\ref{judge:ppt}}\\ \\ \text{Term evaluation} & @m --> m@ & \text{Section~\ref{judge:ev}} \\ \text{Exp evaluation} & @e ==>q e@ & \text{Section~\ref{judge:evm}} \\ \text{Verification} & @|- 'p sign 'p => 'p <# 'p@ & \text{Section~\ref{judge:ver}} \\ \\ \text{Term equivalence} & @m ~~z m : t@ & \text{Section~\ref{judge:eq}} \\ \text{Value equivalence} & @v ~z v : t@ & \text{Section~\ref{judge:eq}} \\ \text{Exp equivalence} & @e ~~z e : t ! q@ & \text{Section~\ref{judge:eeq}} \\ \text{Value equivalence} & @u ~z u : t ! q@ & \text{Section~\ref{judge:eeq}} \\ \text{Type model} & @w |= d@ & \text{Section~\ref{judge:tmodel}} \\ \text{Term model} & @r ~z r : w(g)@ & \text{Section~\ref{judge:mmodel}} \\ \end{array}\]}% \fi\fi \end{document}