1: % end.tex --
2: % Created: 2006/10/23 13:44
3: % Revised: 2007/05/15 10:46
4: %
5: % $Id: end.tex,v 1.10 2007-05-15 15:38:56 jriely Exp $
6: %
7: % ----------------------------------------------------------------------------
8: %
9: % ----------------------------------------------------------------------------
10: \section{Conclusions}
11: \label{sec:end}
12:
13: The focus of this paper is programmatic approaches, such as
14: \JAAS/\DOTNET, that use \RBAC. From a software engineering approach
15: to the design of components, \RBAC\ facilitates a separation
16: of concerns: the design of the system is carried out in terms of
17: a role hierarchy with an associated assignment of permissions to
18: roles, whereas the actual assignment of users to roles takes place
19: at the time of deployment.
20:
21: We have presented two methods to aid the design and use of
22: components that include such access control code. The first ---
23: admittedly standard --- technique enables users of code to deduce
24: the role at which code must be run. The main use of this analysis is
25: to optimize code by enabling the removal of some dynamic checks. The
26: second --- somewhat more novel --- analysis calculates the role that
27: is verified on all execution paths. This analysis is potentially
28: useful in validating architectural security requirements by enabling
29: code designers to deduce the protection guarantees of their code.
30:
31: We have demonstrated the use of these methods by modeling Domain
32: Type Enforcement, as used in SELinux. As future work, we will
33: explore extensions to role polymorphism and recursive roles
34: following the techniques of~\cite{291678,AmaCar93}.
35:
36: % Our paper falls into the broad area of research enlarging the scope of
37: % foundational, language-based security methods
38: % (see~\cite{Schneider+:Language-based:Security,Mitchellsurvey,AbadiMS05}
39: % for surveys). The papers that are most directly relevant to the
40: % current paper are~\cite{BraghinGS04,Adriana2005}. Both these papers
41: % start off with a mobile process-based computational model. Both
42: % calculi have primitives to activate and deactivate roles: these roles
43: % are used to prevent undesired mobility and/or communication, and are
44: % similar to the primitives for role restriction and amplification in
45: % this paper. We expect that our ideas can be adapted to the process
46: % calculi framework. In future work, we also hope to integrate the
47: % powerful bisimulation principles of these papers.
48:
49: % \cite{BraghinGS04,Adriana2005} develop type systems to provide
50: % guarantees about the minimal role required for execution to be
51: % successful --- our first type system occupies the same conceptual
52: % space as this static analysis. However, our second type system that
53: % calculates minimum access controls does not seem to have an analogue
54: % in these papers. More globally, our paper has been influenced by the
55: % desire to serve loosely as a metalanguage for programming \RBAC\
56: % mechanisms in examples such as the \JAAS/\DOTNET\ frameworks. Thus,
57: % our treatment internalizes rights amplification by program combinators
58: % and the amplify role constructor in role lattices. In contrast, the
59: % above papers use external --- i.e. not part of the process language
60: % --- mechanisms (namely, user policies in~\cite{Adriana2005}, and
61: % \RBAC-schemes in~\cite{BraghinGS04}) to enforce control on rights
62: % activation.
63:
64:
65: % Our paper deals with access control, so the extensive work on
66: % information flow, e.g., see~\cite{Sabelfeld:Myers:JSAC} for a survey,
67: % is not directly relevant. However, we note that rights amplification
68: % plays the same role in \lrbac\ that declassification and delimited
69: % release~\cite{DBLP:conf/ccs/ChongM04,DBLP:conf/isss2/SabelfeldM03,DBLP:conf/csfw/MyersSZ04}
70: % plays in the context of information flow; namely that of permitting
71: % access that would not have been possible otherwise. In addition, by
72: % internalizing the ability to amplify code rights into the role
73: % lattice, our system permits access control code to actively
74: % participate in managing rights amplification.
75:
76: \endinput
77: %----------------------------------------------------------------------------
78: % Cut and Paste: Below here everything ignored
79: %----------------------------------------------------------------------------
80:
81: \newpage
82: \begin{example}[Domain-Type Enforcement]
83: \newcommand*{\cpsefliptype}[1]{\overline{#1}}
84: \newcommand*{\jrsefliptype}[1]{\bigl(\tabs{#1}{(\tabs{\atyp}{\tblk{\rleast}{\btyp}})}\bigr)}
85: %%\newcommand*{\cpsefliptype}[1]{FOO(#1)}
86: \newcommand*{\cpsedomtrans}[3]{\RFUNTHREE{dt}{#1}{#2}{#3}}
87: \newcommand*{\cpseassign}[1]{\RFUNONE{assign}{#1}}
88: \begin{sfmath}
89:
90: Define the $\cpsedomtrans{\arol}{\erol}{\brol}$ function by:
91: \begin{displaymath}
92: \cpsedomtrans{\arol}{\erol}{\brol} \eqdef
93: \pabsabs{\afun}{\avar}{
94: \pchk{\pgrd{\arol}{\punit}}
95: \SEMI
96: \pappapp{\afun}{
97: \pgrd{\erol}{\pabsabs{\bfun}{\bvar}{\pmodeq{\brol}{\papp{\bfun}{\bvar}}}}}{
98: \avar}
99: }
100: \end{displaymath}
101: Fix types $\atyp$ and $\btyp$ (for emphasis we use extra
102: parentheses that are not strictly necessary given the usual right
103: associativity for function types).
104: \begin{displaymath}
105: \cpsefliptype{\ctyp} \eqdef
106: \tabs{\ctyp}{(\tabs{\atyp}{\tblk{\rleast}{\btyp}})}
107: \end{displaymath}
108: \begin{displaymath}
109: \cpseassign{\erol} \eqdef
110: \pabsabs{\afun}{\avar}{
111: \pabs{\bvar}{
112: \plet{\bfun}{\pmodeq{\erol}{\pchk{\avar}}}
113: \pappapp{\bfun}{\afun}{\bvar}
114: }
115: }
116: \end{displaymath}
117: \newcommand{\xxx}{\mathcal{F}}
118: Define:
119: \begin{displaymath}
120: \xxx \eqdef {\pabs{\cvar}{\pchk{\pgrd{\brol}{\punit}}}}
121: \end{displaymath}
122: \begin{align*}
123: &
124: \pappapp
125: {\underline{\cpsedomtrans{\arol}{\erol}{\brol}}}
126: {\PBR{\papp{\cpseassign{\erol}}{\xxx}}}
127: {\punit}
128: \\=\;&
129: \pappapp
130: {\PBR{\underline{\pabsabs{\afun}{\avar}{
131: \pchk{\pgrd{\arol}{\punit}}
132: \SEMI
133: \pappapp{\afun}{
134: \PBR{\pgrd{\erol}{\pabsabs{\bfun}{\bvar}{\pmodeq{\brol}{\papp{\bfun}{\bvar}}}}}}{
135: \avar}
136: }}}}
137: {\underline{\PBR{\papp{\cpseassign{\erol}}{\xxx}}}}
138: {\punit}
139: \\\eval\;&
140: \papp
141: {\PBR{\underline{\pabs{\avar}{
142: \pchk{\pgrd{\arol}{\punit}}
143: \SEMI
144: \pappapp{\PBR{\papp{\cpseassign{\erol}}{\xxx}}}{
145: \PBR{\pgrd{\erol}{\pabsabs{\bfun}{\bvar}{\pmodeq{\brol}{\papp{\bfun}{\bvar}}}}}}{
146: \avar}
147: }}}}
148: {\underline{\punit}}
149: \\\eval\;&
150: \underline{\pchk{\pgrd{\arol}{\punit}}}
151: \SEMI
152: \pappapp{\PBR{\papp{\cpseassign{\erol}}{\xxx}}}{
153: \PBR{\pgrd{\erol}{\pabsabs{\bfun}{\bvar}{\pmodeq{\brol}{\papp{\bfun}{\bvar}}}}}}{
154: \punit}
155: \\\eval\;&
156: \pappapp{\PBR{\papp{\underline{\cpseassign{\erol}}}{\xxx}}}{
157: \PBR{\pgrd{\erol}{\pabsabs{\bfun}{\bvar}{\pmodeq{\brol}{\papp{\bfun}{\bvar}}}}}}{
158: \punit}
159: \\=\;&
160: \pappapp{\bigPBR{\papp{
161: \PBR{\underline{\pabsabs{\bfun}{\avar}{
162: \pabs{\bvar}{
163: \plet{\bfun}{\pmodeq{\erol}{\pchk{\avar}}}
164: \pappapp{\bfun}{\afun}{\bvar}
165: }
166: }}}}{\underline{\xxx}}}}{
167: \PBR{\pgrd{\erol}{\pabsabs{\bfun}{\bvar}{\pmodeq{\brol}{\papp{\bfun}{\bvar}}}}}}{
168: \punit}
169: \\\eval\;&
170: \pappapp{
171: \PBR{\underline{\pabs{\avar}{
172: \pabs{\bvar}{
173: \plet{\bfun}{\pmodeq{\erol}{\pchk{\avar}}}
174: \pappapp{\bfun}{\xxx}{\bvar}
175: }
176: }}}}{
177: \PBR{\underline{\pgrd{\erol}{\pabsabs{\bfun}{\bvar}{\pmodeq{\brol}{\papp{\bfun}{\bvar}}}}}}}{
178: \punit}
179: \\\eval\;&
180: \papp{
181: \PBR{\underline{
182: \pabs{\bvar}{
183: \plet{\bfun}{\pmodeq{\erol}{\pchk{{\pgrd{\erol}{\pabsabs{\bfun}{\bvar}{\pmodeq{\brol}{\papp{\bfun}{\bvar}}}}}}}}
184: \pappapp{\bfun}{\xxx}{\bvar}
185: }
186: }}}{
187: \underline{\punit}}
188: \\\eval\;&
189: \plet{\bfun}{\pmodeq{\erol}{\underline{\pchk{{\pgrd{\erol}{\pabsabs{\bfun}{\bvar}{\pmodeq{\brol}{\papp{\bfun}{\bvar}}}}}}}}}
190: \pappapp{\bfun}{\xxx}{\punit}
191: \\\eval\;&
192: \plet{\bfun}{\underline{\pmodeq{\erol}{\pblk{\pabsabs{\bfun}{\bvar}{\pmodeq{\brol}{\papp{\bfun}{\bvar}}}}}}}
193: \pappapp{\bfun}{\xxx}{\punit}
194: \\\eval\;&
195: \underline{\plet{\bfun}{\pblk{\pabsabs{\bfun}{\bvar}{\pmodeq{\brol}{\papp{\bfun}{\bvar}}}}}
196: \pappapp{\bfun}{\xxx}{\punit}}
197: \\\eval\;&
198: \pappapp{\PBR{\underline{\pabsabs{\bfun}{\bvar}{\pmodeq{\brol}{\papp{\bfun}{\bvar}}}}}}{\underline{\xxx}}{\punit}
199: \\\eval\;&
200: \papp{\PBR{\underline{\pabs{\bvar}{\pmodeq{\brol}{\papp{\xxx}{\bvar}}}}}}{\underline{\punit}}
201: \\\eval\;&
202: \pmodeq{\brol}{\papp{\underline{\xxx}}{\punit}}
203: \\=\;&
204: \pmodeq{\brol}{\papp{\PBR{\underline{\pabs{\cvar}{\pchk{\pgrd{\brol}{\punit}}}}}}{\underline{\punit}}}
205: \\\eval\;&
206: \pmodeq{\brol}{\underline{\pchk{\pgrd{\brol}{\punit}}}}
207: \\\eval\;&
208: \underline{\pmodeq{\brol}{\pblk{\punit}}}
209: \\\eval\;&
210: \pblk{\punit}
211: \end{align*}
212: \begin{displaymath}
213: \soktrm{}{
214: \cpsedomtrans{\arol}{\erol}{\brol}
215: }{
216: \tabs{
217: \cpsefliptype{
218: \tgrd{
219: \erol}{
220: \cpsefliptype{
221: \tabs{
222: \atyp}{
223: \tblk{\brol}{\btyp}
224: }
225: }
226: }
227: }
228: }{
229: (\tabs{
230: \atyp}{
231: \tblk{\arol}{\btyp}
232: })
233: }
234: }
235: \end{displaymath}
236: \begin{displaymath}
237: \soktrm{}{\cpseassign{\erol}}{
238: \tabs{
239: (\tabs{
240: \atyp}{
241: \tblk{\brol}{\btyp}
242: })
243: }{
244: \cpsefliptype{
245: \tgrd{
246: \erol}{
247: \cpsefliptype{
248: \tabs{
249: \atyp}{
250: \tblk{\brol}{\btyp}
251: }
252: }
253: }
254: }
255: }
256: }
257: \end{displaymath}
258: \begin{displaymath}
259: \soktrm{}{
260: \cpsedomtrans{\arol}{\erol}{\brol}
261: }{
262: \tabs{
263: \jrsefliptype{
264: \tgrd{
265: \erol}{
266: \jrsefliptype{
267: \tabs{
268: \atyp}{
269: \tblk{\brol}{\btyp}
270: }
271: }
272: }
273: }
274: }{
275: (\tabs{
276: \atyp}{
277: \tblk{\arol}{\btyp}
278: })
279: }
280: }
281: \end{displaymath}
282: \begin{displaymath}
283: \soktrm{}{\cpseassign{\erol}}{
284: \tabs{
285: (\tabs{
286: \atyp}{
287: \tblk{\brol}{\btyp}
288: })
289: }{
290: \jrsefliptype{
291: \tgrd{
292: \erol}{
293: \jrsefliptype{
294: \tabs{
295: \atyp}{
296: \tblk{\brol}{\btyp}
297: }
298: }
299: }
300: }
301: }
302: }
303: \end{displaymath}
304: So the functional composition of $\cpseassign{\arol}$ and
305: $\cpsedomtrans{\arol}{\erol}{\brol}$ has type:
306: \begin{displaymath}
307: \tabs{
308: (\tabs{
309: \atyp}{
310: \tblk{\brol}{\btyp}
311: })
312: }{
313: (\tabs{
314: \atyp}{
315: \tblk{\arol}{\btyp}
316: })
317: }
318: \end{displaymath}
319:
320:
321:
322: With the $\setrans{}{}{}$ and $\seassign{}$ functions we can adapt
323: the login example from \cite{dte:confining-root-programs} to
324: $\lrbac$. In this example, the \DTE\ mechanism is used to force
325: every invocation of user code (running at $\ruser$) from daemon
326: code (running at $\rdaemon$) to occur via trusted login code
327: (running at $\rlogin$). This is achieved by providing domain
328: transitions from $\rdaemon$ to $\rlogin$, and $\rlogin$ to
329: $\ruser$, but no others. Moreover, code permitted to run at
330: $\rlogin$ must be assigned \DTE\ type $\xlogin$, and similarly for
331: $\ruser$ and $\xuser$. Thus a full program running daemon code
332: $\atrm$ has the following form, where $M$ contains no direct
333: rights amplification.
334: %
335: \allowdisplaybreaks
336: \begin{displaymath}
337: \begin{array}{l}
338: \pletchk{\setransdl}{\setrans{\rdaemon}{\xlogin}{\rlogin}}{} \\
339: \pletchk{\setranslu}{\setrans{\rlogin}{\xuser}{\ruser}}{} \\
340: \pletchk{\seassignu}{\seassign{\xuser}}\\
341: \pletchk{\seassignl}{\seassign{\xlogin}}\\
342: \plet{\seshell}{\papp{\seassignu}{\pabsp{}{\ldots}}} \\
343: \pletNOSEMI{\selogin}{
344: \papp{\seassignl}{
345: (\pabs{\sepwd}{
346: \begin{array}[t]{l}
347: \pletchk{z}{\setranslu}\\
348: \pcond{\sepwd\eqstr\text{"secret"}}{\papp{\papp{z}{\seshell}}{\punit}}{\ldots}
349: )\SEMI
350: \end{array}
351: }}}
352: \\
353: \pmoddn{\rdaemon}{\atrm}
354: \end{array}
355: \end{displaymath}
356: Because $\selogin$ provides the sole transition to $\ruser$, the
357: daemon code $\atrm$ must provide the correct password in order to
358: execute the shell at $\ruser$. In addition, removal of the domain
359: transition $\setransdl$ makes it impossible for the daemon code to
360: execute any code at $\ruser$.
361: \end{sfmath}
362: \qed
363: \end{example}
364: \newpage
365:
366: % Local Variables:
367: % mode: latex
368: % TeX-master: "sub"
369: % End:
370: