% -*- LaTeX -*- \documentclass[12pt]{seminar} \special{!TeXDict begin /landplus90{true} store end} \usepackage{color,pstcol,url,amstext,alltt,stmaryrd} \usepackage{code} \centerslidesfalse %\pagestyle{empty} \slideframe{none} \newcommand{\N}[1]{\text{\rm\ttfamily\mdseries{#1}}} \newcommand{\B}[1]{{\textcolor{blue}{#1}}} \newcommand{\R}[1]{{\red{#1}}} \newcommand{\F}[1]{{\bf{#1}}} \newcommand{\FL}[1]{{\bf\large{#1}}} \newcommand{\E}[1]{{\em{#1}}} \newcommand{\EB}[1]{{\blue\em{#1}}} \newcommand{\ER}[1]{{\red\em{#1}}} \newcommand{\tight}{\vskip-2ex} \newcommand{\head}[1]{{\blue\bf\Large #1}\vskip1ex\hrule\vskip3ex} \newcommand{\topic}[1]{\hrule\center\vskip20ex{\sc\blue\LARGE #1}\vskip20ex\hrule} \newcommand{\point}{{\red@\hookrightarrow@}\quad} \newcommand{\Rule}[3]{\infer{#2}{#3} & \raisebox{1.5ex}{\text{(#1)}} \\\\} \newcommand{\Cite}[1]{{\footnotesize\gray [#1]}} \begin{document} \begin{slide} \hrule\vskip6ex \begin{center} {\blue\bf\Large Run-time Principals in} \vskip1ex {\blue\bf\Large Information-flow Type Systems} \vskip6ex {\large Stephen Tse \qquad Steve Zdancewic} \vskip1ex {\large University of Pennsylvania} \end{center} \vskip7ex \begin{flushright} {\footnotesize\gray IEEE Symposium on Security and Privacy, May 2004} \end{flushright} \hrule \end{slide} \begin{slide} \head{Building secure software} \tight {\bf\large Goal:} help programmers build secure software that interacts with existing \EB{security infrastructure} such as authentication, file permissions, cryptography... \end{slide} \begin{slide} \head{Building secure software} \tight {\bf\large Goal:} help programmers build secure software that interacts with existing \EB{security infrastructure} such as authentication, file permissions, cryptography... \bigskip {\bf\large Challenges:} \begin{enumerate} \item Increasingly large and distributed \EB{applications} \end{enumerate} \end{slide} \begin{slide} \head{Building secure software} \tight {\bf\large Goal:} help programmers build secure software that interacts with existing \EB{security infrastructure} such as authentication, file permissions, cryptography... \bigskip {\bf\large Challenges:} \begin{enumerate} \item Increasingly large and distributed \EB{applications} \item Increasingly complex and refined \EB{policies}: \\ type safety, secrecy, integrity \end{enumerate} \end{slide} \begin{slide} \head{Building secure software} \tight {\bf\large Goal:} help programmers build secure software that interacts with existing \EB{security infrastructure} such as authentication, file permissions, cryptography... \bigskip {\bf\large Challenges:} \begin{enumerate} \item Increasingly large and distributed \EB{applications} \item Increasingly complex and refined \EB{policies}: \\ type safety, secrecy, integrity \item Existing mechanisms (e.g. PKI, OS) are crucial but higher levels of \EB{abstraction} are needed \end{enumerate} \end{slide} \begin{slide} \head{Language-based security} \tight {\bf\large Our approach:} design type systems for specifying high-level policies and providing strong static guarantees \bigskip {\bf\large Long History:} Lattice model \Cite{Denning, 1976}, Jif \Cite{Myers et. al, 1998}, Flow Caml \Cite{Pottier and Simonet, 2003}, ... \end{slide} \begin{slide} \head{Language-based security} \tight {\bf\large Our approach:} design type systems for specifying high-level policies and providing strong static guarantees \bigskip {\bf\large Long History:} Lattice model \Cite{Denning, 1976}, Jif \Cite{Myers et. al, 1998}, Flow Caml \Cite{Pottier and Simonet, 2003}, ... \begin{enumerate} \item Programmers specify policies as \EB{type annotations} \item Compilers automatically catch \EB{illegal info flows} \end{enumerate} \begin{alltt} String\B{\{H\}} password = "secret"; void print (String\B{\{L\}} x) \{...\} \end{alltt} \bigskip \begin{flushright} \B{\large{\em {Connect infrastructures and languages?}}} \end{flushright} \end{slide} \begin{slide} \head{Compile time vs. run time} \begin{itemize} \item Most existing security languages specify policies known at \ER{compile time} \begin{alltt} String\B{\{H\}} password = "secret"; void print (String\B{\{L\}} x) \{...\} \end{alltt} \end{itemize} \end{slide} \begin{slide} \head{Compile time vs. run time} \begin{itemize} \item Most existing security languages specify policies known at \ER{compile time} \begin{alltt} String\B{\{H\}} password = "secret"; void print (String\B{\{L\}} x) \{...\} \end{alltt} \item But existing infrastructures express constraints in terms of \EB{principals} known only at \ER{run time} \begin{enumerate} \item authentication: \EB{public key} from PKI \item file permissions: \EB{user id} from OS \end{enumerate} \end{itemize} \end{slide} \begin{slide} \head{Compile time vs. run time} \E{How to interact with run-time systems?} \begin{enumerate} \item determine run-time principals from run-time systems \item specify security policies in term of such principals \item connect compile-time principals (e.g. \B{root}) with run-time principals (e.g. \B{user}) \end{enumerate} \medskip \begin{alltt} \R{principal} user = Runtime.getUser(); \medskip void print (String\B{\{user:\}} x) \{\ldots\} \medskip void printroot (String\B{\{root:\}} y) \{ \R{if}\ (user \R{==} root) print(y); \} \end{alltt} \end{slide} \begin{slide} \head{Technical challenges} \begin{enumerate} \item Formalize typing and evaluation of such a language \item Prove the soundness and noninterference theorems \item Allow downgrading information \item Implement over a distributed system \end{enumerate} \end{slide} \begin{slide} \head{Language features} \begin{tabular}{lrcl} & \fbox{\blue Expression @e@} && \fbox{\blue Type @t@} \\ principal\mbox{\hskip8ex} & @root@ &:& @\#root@ \end{tabular} \bigskip The expression \B{@root@} is a principal constant, known at \ER{compile time}, and has the \ER{principal type} \B{@\#root@}. % The principal type \B{@\#root@} has the singleton property % that only the principal \B{@root@} has such a type. This property allows % the type system to precisely analyze principals at compile time. \end{slide} \begin{slide} \head{Language features} \begin{tabular}{lrcl} & \fbox{\blue Expression @e@} && \fbox{\blue Type @t@} \\ principal\mbox{\hskip8ex} & @root@ &:& @\#root@ \\ variable & @id@ &:& @\#user@ \end{tabular} \bigskip The expression \B{@id@} is a principal variable (a first-class construct), known at \ER{run time}, and has type \B{@\#user@}. \end{slide} \begin{slide} \head{Language features} \begin{tabular}{lrcl} & \fbox{\blue Expression @e@} && \fbox{\blue Type @t@} \\ principal\mbox{\hskip8ex} & @root@ &:& @\#root@ \\ variable & @id@ &:& @\#user@ \end{tabular} \bigskip The expression \B{@id@} is a principal variable (a first-class construct), known at \ER{run time}, and has type \B{@\#user@}. \smallskip Universal and existential polymorphism: \begin{enumerate} \item @void print\R{}\ (\#user id,\ int\B{[user:]}\ x) [..]@ \item @\R{\#user}\ id = Runtime.getUser();@ \end{enumerate} \end{slide} \begin{slide} \head{Language features} \tight \begin{tabular}{lrcl} & \fbox{\blue Expression @e@} && \fbox{\blue Type @t@} \\ principal & @root@ &:& @\#root@ \\ variable & @id@ &:& @\#user@ \\ delegation & @if (id <: root) e1 e2@ &:& @t@ \end{tabular} \bigskip Delegation (or acts-for) relation \R{@id <: root@} is an order on principals. \Cite{Abadi, Burrows, Lampson, Plotkin} \end{slide} \begin{slide} \head{Security theorems} {\bf Soundness:} If @|- e : t@, then @e -->* v@. \begin{quote} \it A well-typed program does not generate any run-time errors. \end{quote} \end{slide} \begin{slide} \head{Security theorems} {\bf Soundness:} If @|- e : t@, then @e -->* v@. \begin{quote} \it A well-typed program does not generate any run-time errors. \end{quote} \bigskip {\bf Noninterference:} If @x:int\B{[H]} |- e : bool\B{[L]}@ and @|- v1 : int\B{[H]}@ and @|- v2:int\B{[H]}@, then @e\{v1/x\} -->* v@ iff @e\{v2/x\} -->* v@. \begin{quote} \it If an observer @e@ is a well-typed Boolean program of low-security @bool\B{[L]}@, then @e@ cannot distinguish possibly different values such as @v1,v2@ of higher security @int\B{[H]}@. \end{quote} % \F{Logical relations}: extend equivalence to higher-order types % (functions), label, principals, and polymorphism. \end{slide} \begin{slide} \head{Declassification and DLM} \tight \begin{itemize} \item Noninterference provides a strong \EB{static guarantee} but it is too restrictive for practical programming \\ \point Idea: declassification \\ \point Challenge: regulate its use \end{itemize} \end{slide} \begin{slide} \head{Declassification and DLM} \tight \begin{itemize} \item Noninterference provides a strong \EB{static guarantee} but it is too restrictive for practical programming \\ \point Idea: declassification \\ \point Challenge: regulate its use \item Decentralized label model \Cite{Myers, Liskov} \\ \point Labels: \B{@[Alice:Bob,Chris;\quad Dave:Bob]@} \\ \point @Alice@ and @Dave@ are the \EB{owners} of the data \\ \point Both @Alice@'s and @Dave@'s policies are enforced \end{itemize} \end{slide} \begin{slide} \head{Declassification and DLM} \tight \begin{itemize} \item Noninterference provides a strong \EB{static guarantee} but it is too restrictive for practical programming \\ \point Idea: declassification \\ \point Challenge: regulate its use \item Decentralized label model \Cite{Myers, Liskov} \\ \point Labels: \B{@[Alice:Bob,Chris;\quad Dave:Bob]@} \\ \point @Alice@ and @Dave@ are the \EB{owners} of the data \\ \point Both @Alice@'s and @Dave@'s policies are enforced \item Jif: DLM + robust declassification \Cite{Myers et al.} \\ \point Idea: owner has the \EB{authority} to declassify \\ \point Challenge: authority for run-time principals \end{itemize} \end{slide} \begin{slide} \head{Authority and certificates} \begin{itemize} \item Acquisition: obtain a certificate that says Alice \EB{grants} the authority of declassifying to Bob \qquad @cert c = \R{acquire}\ Alice\ \R{#>}\ Declassify Bob@ \end{itemize} \end{slide} \begin{slide} \head{Authority and certificates} \begin{itemize} \item Acquisition: obtain a certificate that says Alice \EB{grants} the authority of declassifying to Bob \qquad @cert c = \R{acquire}\ Alice\ \R{#>}\ Declassify Bob@ \bigskip General form of authority: @X\ \R{#>}\ i@ @X@ is a principal and @i@ is a \EB{privilege} such as \begin{enumerate} \item @Delegate ATM@: \quad \textit{``allow @ATM@ to act for @X@''} \item @Declassify Net@: \textit{``allow declassifying @X@'s data''} \item @Withdraw 100@: \quad \textit{``allow debiting @X@'s account''} \end{enumerate} \end{itemize} \end{slide} \begin{slide} \head{Authority and certificates} \begin{itemize} \item Acquisition: obtain a certificate that says Alice \EB{grants} the authority of declassifying to Bob \qquad @cert c = \R{acquire}\ Alice\ \R{#>}\ Declassify Bob@ \item Verification: determine whether a certificate \EB{implies} that Alice \EB{grants} the authority of declassifying to Bob \qquad @\R{if}\ (c\ \R{=>}\ Alice\ \R{#>}\ Declassify Bob) e1 e2@ \end{itemize} \end{slide} \begin{slide} \head{Authority and certificates} \begin{itemize} \item Acquisition: obtain a certificate that says Alice \EB{grants} the authority of declassifying to Bob \qquad @cert c = \R{acquire}\ Alice\ \R{#>}\ Declassify Bob@ \item Verification: determine whether a certificate \EB{implies} that Alice \EB{grants} the authority of declassifying to Bob \qquad @\R{if}\ (c\ \R{=>}\ Alice\ \R{#>}\ Declassify Bob) e1 e2@ \item Access control and Java stack inspection \Cite{Appel, Felton, Wallach; Fournet, Gordon; Pottier, Skalka, Smith} \item Robust declassification \Cite{Myers, Zdancewic} \end{itemize} \end{slide} \begin{slide} \head{Application: distributed banking} {\footnotesize\leftmargini=0in \begin{code} void main (...) \{ ... \} \end{code}} \begin{itemize} \item Distributed system between ATM and Bank server \item Customer is a \EB{run-time} principal \item Customer delegates to ATM for bank service \item Certificates are created and logged for audit purpose \item For brevity, assume a secure network is established \end{itemize} \end{slide} \begin{slide} \head{Application: distributed banking} {\footnotesize\leftmargini=0in\setlength\baselineskip{1.3\baselineskip} \begin{code} void main (cert cnet) \{ \#user\B{\{ATM:\}} id = login(); cert cdel = \R{acquire} id \R{@#>@} Delegate ATM; ... \} \end{code}} \end{slide} \begin{slide} \head{Application: distributed banking} {\footnotesize\leftmargini=0in\setlength\baselineskip{1.3\baselineskip} \begin{code} void main (cert cnet) \{ \#user\B{\{ATM:\}} id = login(); cert cdel = \R{acquire} id \R{@#>@} Delegate ATM; cert creq = \R{acquire} id \R{@#>@} Withdraw 100; Msg\B{\{ATM:\}} m = new Msg(id, cdel, creq); ... \} \end{code}} \end{slide} \begin{slide} \head{Application: distributed banking} {\footnotesize\leftmargini=0in\setlength\baselineskip{1.3\baselineskip} \begin{code} void main (cert cnet) \{ \#user\B{\{ATM:\}} id = login(); cert cdel = \R{acquire} id \R{@#>@} Delegate ATM; cert creq = \R{acquire} id \R{@#>@} Withdraw 100; Msg\B{\{ATM:\}} m = new Msg(id, cdel, creq); ... Msg\B{\{ATM:Net\}} x = \R{declassify} m as Msg\B{\{ATM:Net\}}; int\B{\{user:\}} balance = request(x); ... \} \end{code}} \end{slide} \begin{slide} \head{Application: distributed banking} {\footnotesize\leftmargini=0in\setlength\baselineskip{1.3\baselineskip} \begin{code} void main (cert cnet) \{ \#user\B{\{ATM:\}} id = login(); cert cdel = \R{acquire} id \R{@#>@} Delegate ATM; cert creq = \R{acquire} id \R{@#>@} Withdraw 100; Msg\B{\{ATM:\}} m = new Msg(id, cdel, creq); \R{if}\ (cnet \R{@=>@} ATM \R{@#>@} Declassify Net) \{ Msg\B{\{ATM:Net\}} x = \R{declassify} m as Msg\B{\{ATM:Net\}}; int\B{\{user:\}} balance = request(x); ... \} \} \end{code}} \end{slide} \begin{slide} \head{Abstract implementation} The run-time system of our language must maintain \EB{principal hierarchy} and \EB{authority certificates}. Specifically: \begin{enumerate} \item Principal: \R{@X@} \item Delegation test: @\R{if}\ (X1\ \R{<:}\ X2)..@ \item Capability and authority: @X\R{[}i\R{]}@ and @X\ \R{#>}\ i@ \item Privileges: @\R{Delegate}\ X@ and @\R{Declassify}\ X@ \item Certificate acquisition: @\R{acquire}\ X\ \R{#>}\ i@ \item Certificate verification: @\R{if}\ (c\ \R{=>}\ X\ \R{#>}\ i)..@ \end{enumerate} \end{slide} \begin{slide} \head{PKI implementation} PKI naturally supports \EB{distributed} access control: \begin{tabular}{lrcll} \quad principal & @X@ &@\R{-->}@& @K_X@ & public key \\ \quad delegate & @Del X@ &@\R{-->}@& @(DEL,K_X)@ & certificate contents \\ \quad declassify & @Dcls X@ &@\R{-->}@& @(DCLS,K_X)@ & certificate contents \medskip \\ \quad capability & @X[i]@ &@\R{-->}@& @K^{-1}_X[i]@ & digital certificate \\ \quad authority & @X#>i@ &@\R{-->}@& @(K_X,i)@ & public key, privilege \end{tabular} \bigskip Delegation tests and certificate verification are mapped to comparing public keys in the \EB{delegation chain} and \EB{cryptographic verification}. \Cite{Chothia, Duggan, Vitek; ...} \end{slide} \begin{slide} \head{Conclusion} \begin{itemize} \item {\bf Scope:} language-based security in decentralized label model with declassification \item {\bf Contributions:} connect \B{\em compile-time} and \B{\em run-time} principals in a sound type system \item {\bf Features:} allow programmers to express policies that interact with existing security infrastructures \bigskip \item Apollo project: interpreter with monadic labels \\ \point \url{http://www.cis.upenn.edu/~stse/apollo} \item Security-Oriented Languages (SOL) \\ \point \url{http://www.cis.upenn.edu/~stevez/sol} \end{itemize} \end{slide} \end{document}