nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

JRIF: Reactive Information Flow Control for Java

verfasst von : Elisavet Kozyri, Owen Arden, Andrew C. Myers, Fred B. Schneider

Erschienen in: Foundations of Security, Protocols, and Equational Reasoning

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

A reactive information flow (RIF) automaton for a value v specifies (i) restrictions on uses for v and (ii) the RIF automaton for any value that might be derived from v. RIF automata thus specify how transforming a value alters restrictions for the result. As labels, RIF automata are both expressive and intuitive vehicles for describing allowed information flows. JRIF is a dialect of Java that uses RIF automata for specifying information flow control policies. The implementation of JRIF involved replacing the information flow type system of the Jif language by a RIF-based type system. JRIF demonstrates (i) the practicality and utility of RIF automata, and (ii) the ease with which an existing information flow control system can be modified to support the expressive power of RIF automata.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Robust Declassification by Incremental Typing

Nächstes Kapitel Symbolic Timed Trace Equivalence

Reclassifiers that do not trigger a transition between states (i.e., self-transitions) need not be specified explicitly, thereby permitting compact representation of \(\delta \), as we illustrate in Sect. 3.

This example thus addresses only a subset of information flow policies that a conference system needs to satisfy [15].

This example is inspired by TruDocs [32].

For clarity, the syntax presented in this section simplifies the syntax actually used in our JRIF implementation.

We focus only on confidentiality for this example.

\(\mathcal {R}(\langle Q,\varSigma ,\delta ,q_0, Prins \rangle )\triangleq Prins (q_0)\).

\(\mathcal {T}(\langle Q,\varSigma ,\delta ,q_0, Prins \rangle ,\textsf {\textit{F}})\triangleq \langle Q,\varSigma ,\delta ,\delta ^*(q_0,\textsf {\textit{F}}), Prins \rangle \). Here \(\delta ^*\) is the transitive closure of \(\delta \): \(\delta ^*(q_0,\textsf {\textit{F}}' \mathsf {f_{}})\triangleq \delta (\delta ^*(q_0,\textsf {\textit{F}}'), \mathsf {f_{}})\) and \(\delta ^*(q_0,\epsilon )\triangleq q_0\), where \(\epsilon \) denotes the empty sequence.

The product of two c-automata \(\lambda _c=\langle Q,\varSigma ,\delta ,q_0, Prins \rangle \) and \(\lambda _c'=\langle Q',\varSigma ',\delta ',q_0', Prins '\rangle \) is defined to be \( \lambda _c\sqcup _c\lambda _c'\triangleq \langle Q\times Q',\varSigma \cup \varSigma ',\delta _\times ,\langle q_0,q_0' \rangle , Prins _\times \rangle \) where \(\delta _\times \) and \( Prins _\times \) are defined for \(\langle q,q' \rangle \in Q\times Q'\) as: \( \delta _\times (\langle q,q' \rangle , \mathsf {f_{}})\triangleq \langle \delta (q, \mathsf {f_{}}),\delta '(q', \mathsf {f_{}}) \rangle , \) and \( Prins _\times (\langle q,q' \rangle )\triangleq Prins (q)\cap Prins '(q'). \) The definition for the product of two i-automata is the same with the only difference being the definition of \( Prins _\times \), where instead of intersection we take the union of sets. RIF automata form a lattice.

Label checking rules for Java features already exist in Jif. Their core component is a call to a decision algorithm for the restrictiveness relation. So, we were able to support JRIF labels simply by substituting Jif’s decision algorithm with JRIF’s decision algorithm for JRIF label restrictiveness.

Classic labels can be simulated by one-state RIF automata.

Source code for this shared calendar implementation in JRIF can be found on JRIF’s web page [17].

The source code for JRIF can be found on JRIF’s web page [17].

Askarov, A., Sabelfeld, A.: Gradual release: unifying declassification, encryption and key release policies. In: IEEE Symposium on Security and Privacy, pp. 207–221 (2007). https://doi.org/10.1109/SP.2007.22

Banerjee, A., Naumann, D., Rosenberg, S.: Expressive declassification policies and modular static enforcement. In: IEEE Symposium on Security and Privacy, pp. 339–353 (2008). https://doi.org/10.1109/SP.2008.20

Bell, E.D., LaPadula, J.L.: Secure computer systems: mathematical foundations (1973)

Broberg, N., van Delft, B., Sands, D.: Paragon for practical programming with information-flow control. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 217–232. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-03542-0_16CrossRefMATH

Broberg, N., Sands, D.: Flow locks: towards a core calculus for dynamic flow policies. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 180–196. Springer, Heidelberg (2006). https://doi.org/10.1007/11693024_13CrossRef

Cheng, W., et al.: Abstractions for usable information flow control in Aeolus. In: Proceedings of the 2012 USENIX Conference on Annual Technical Conference, USENIX ATC 2012, p. 12. USENIX Association, Berkeley (2012). http://dl.acm.org/citation.cfm?id=2342821.2342833

Chong, S., Myers, A.: End-to-end enforcement of erasure and declassification. In: 2008 IEEE 21st Computer Security Foundations Symposium, CSF 2008, pp. 98–111 (2008). https://doi.org/10.1109/CSF.2008.12

Denning, D.E.R.: Secure information flow in computer systems. Ph.D. thesis, West Lafayette, IN, USA (1975)

Efstathopoulos, P., et al.: Labels and event processes in the Asbestos operating system. In: Proceedings of the Twentieth ACM Symposium on Operating Systems Principles, SOSP 2005, pp. 17–30. ACM, New York (2005). https://doi.org/10.1145/1095810.1095813

10.

Elnikety, E., Garg, D., Druschel, P.: SHAI: enforcing data-specific policies with near-zero runtime overhead. Technical report, Max Planck Institute for Software Systems, Saarland Informatics Campus, Germany, January 2018

11.

Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11–20 (1982)

12.

Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. Int. J. Inf. Secur. 8(6), 399–422 (2009). https://doi.org/10.1007/s10207-009-0086-1CrossRef

13.

Hicks, B., King, D., McDaniel, P., Hicks, M.: Trusted declassification: high-level policy for a security-typed language. In: Proceedings of the 2006 Workshop on Programming Languages and Analysis for Security, PLAS 2006, pp. 65–74. ACM, New York (2006). https://doi.org/10.1145/1134744.1134757

14.

Johnson, A., Waye, L., Moore, S., Chong, S.: Exploring and enforcing security guarantees via program dependence graphs. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pp. 291–302. ACM, New York (2015). https://doi.org/10.1145/2737924.2737957

15.

Kanav, S., Lammich, P., Popescu, A.: A conference management system with verified document confidentiality. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 167–183. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_11CrossRef

16.

Kozyri, E.: Enhancing expressiveness of information flow labels: reclassification and permissiveness. Ph.D. thesis, Ithaca, NY, USA (2018)

17.

Kozyri, E., Arden, O., Myers, A.C., Schneider, F.B.: JRIF: Java with Reactive Information Flow, February 2016. Software release http://www.cs.cornell.edu/jrif/

18.

Krohn, M., et al.: Information flow control for standard OS abstractions. In: Proceedings of Twenty-First ACM SIGOPS Symposium on Operating Systems Principles, SOSP 2007, pp. 321–334. ACM, New York (2007). https://doi.org/10.1145/1294261.1294293

19.

Li, P., Zdancewic, S.: Downgrading policies and relaxed noninterference. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, pp. 158–170. ACM, New York (2005). https://doi.org/10.1145/1040305.1040319

20.

Li, P., Zdancewic, S.: Practical information-flow control in web-based information systems. In: Proceedings of the 18th IEEE Workshop on Computer Security Foundations, CSFW 2005, pp. 2–15. IEEE Computer Society, Washington, DC (2005). https://doi.org/10.1109/CSFW.2005.23

21.

Myers, A.C., Zheng, L., Zdancewic, S., Chong, S., Nystrom, N.: JIF 3.0: Java Information Flow. Software release http://www.cs.cornell.edu/jif, July 2006

22.

Myers, A.C.: JFlow: Practical mostly-static information flow control. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1999, pp. 228–241. ACM, New York (1999). https://doi.org/10.1145/292540.292561

23.

Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: Proceedings of the Sixteenth ACM Symposium on Operating Systems Principles, SOSP 1997, pp. 129–142. ACM, New York (1997). https://doi.org/10.1145/268998.266669

24.

Pottier, F., Conchon, S.: Information flow inference for free. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, ICFP 2000, pp. 46–57. ACM, New York (2000). https://doi.org/10.1145/351240.351245

25.

Rocha, B., Bandhakavi, S., den Hartog, J., Winsborough, W., Etalle, S.: Towards static flow-based declassification for legacy and untrusted programs. In: IEEE Symposium on Security and Privacy, pp. 93–108 (2010). https://doi.org/10.1109/SP.2010.14

26.

Rocha, B., Conti, M., Etalle, S., Crispo, B.: Hybrid static-runtime information flow and declassification enforcement. IEEE Trans. Inf. Forensics Secur. 8(8), 1294–1305 (2013). https://doi.org/10.1109/TIFS.2013.2267798CrossRef

27.

Roy, I., Porter, D.E., Bond, M.D., McKinley, K.S., Witchel, E.: Laminar: practical fine-grained decentralized information flow control. In: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, pp. 63–74. ACM, New York (2009). https://doi.org/10.1145/1542476.1542484

28.

Rushby, J.: Noninterference, transitivity and channel-control security policies. Technical report (1992)

29.

Sabelfeld, A., Myers, A.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003). https://doi.org/10.1109/JSAC.2002.806121CrossRef

30.

Sabelfeld, A., Myers, A.C.: A model for delimited information release. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 174–191. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-37621-7_9CrossRef

31.

Sabelfeld, A., Sands, D.: Declassification: dimensions and principles. J. Comput. Secur. 17(5), 517–548 (2009). http://dl.acm.org/citation.cfm?id=1662658.1662659

32.

Schneider, F.B., Walsh, K., Sirer, E.G.: Nexus Authorization Logic (NAL): design rationale and applications. ACM Trans. Inf. Syst. Secur. 14(1), 8:1–8:28 (2011). https://doi.org/10.1145/1952982.1952990CrossRef

33.

Stefan, D., Russo, A., Mitchell, J.C., Mazières, D.: Flexible dynamic information flow control in Haskell. In: Proceedings of the 4th ACM Symposium on Haskell, Haskell 2011, pp. 95–106. ACM, New York (2011). https://doi.org/10.1145/2034675.2034688

34.

Volpano, D., Irvine, C., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2–3), 167–187 (1996). http://dl.acm.org/citation.cfm?id=353629.353648

35.

Zeldovich, N., Boyd-Wickizer, S., Kohler, E., Mazières, D.: Making information flow explicit in HiStar. In: Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation-Volume 7, OSDI 2006, p. 19. USENIX Association, Berkeley (2006). http://dl.acm.org/citation.cfm?id=1267308.1267327

36.

Zheng, L., Myers, A.C.: Dynamic security labels and static information flow control. Int. J. Inf. Secur. 6(2), 67–84 (2007). https://doi.org/10.1007/s10207-007-0019-9CrossRef

Titel: JRIF: Reactive Information Flow Control for Java
verfasst von: Elisavet Kozyri
Owen Arden
Andrew C. Myers
Fred B. Schneider
Verlag: Springer International Publishing
Buch: Foundations of Security, Protocols, and Equational Reasoning
Print ISBN: 978-3-030-19051-4

Electronic ISBN: 978-3-030-19052-1

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-19052-1_7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"