Restrictions that a reactive information flow (RIF) label imposes on a value are determined by the sequence of operations used to derive that value. This allows declassification, endorsement, and other forms of reclassification to be supported in a uniform way. Piecewise noninterference (PWNI) is introduced as a fitting security policy, because noninterference is not suitable. A type system is given for static enforcement of PWNI in programs that associate checkable classes of RIF labels with variables. Two checkable classes of RIF labels are described: RIF automata are general-purpose and based on finite-state automata; κ-labels concern confidentiality in programs that use cryptographic operations.
M.Abadi and C.Fournet, Access control based on execution history, in: Proceedings of the 10th Annual Network and Distributed System Security Symposium, 2003, pp. 107–121.
A.Askarov and A.Sabelfeld, Gradual release: Unifying declassification, encryption and key release policies, in: Proceedings of the IEEE Symposium on Security and Privacy, 2007, pp. 207–221. doi:10.1109/SP.2007.22.
4.
A.Askarov and A.Sabelfeld, Localized delimited release: Combining the what and where dimensions of information release, in: Proceedings of the 2007 Workshop on Programming Languages and Analysis for Security, PLAS’07, ACM, New York, NY, USA, 2007, pp. 53–60. doi:10.1145/1255329.1255339.
5.
T.H.Austin and C.Flanagan, Multiple facets for dynamic information flow, in: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’12, ACM, New York, NY, USA, 2012, pp. 165–178. doi:10.1145/2103656.2103677.
6.
T.H.Austin, J.Yang, C.Flanagan and A.Solar-Lezama, Faceted execution of policy-agnostic programs, in: Proceedings of the 8th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, PLAS’13, ACM, New York, NY, USA, 2013, pp. 15–26.
7.
A.Banerjee, D.A.Naumann and S.Rosenberg, Expressive declassification policies and modular static enforcement, in: Proceedings of the IEEE Symposium on Security and Privacy, 2008, pp. 339–353. doi:10.1109/SP.2008.20.
8.
D.Bell and L.La Padula, Secure computer systems: Unified exposition and MULTICS interpretation, Technical Report ESD-TR-75306, Bedford, MA, 1976.
9.
E.Birrell and F.B.Schneider, A reactive approach to use-based privacy, Technical Report 54843, Cornell University, Computing and Information Science, November 2017.
10.
N.Broberg, B.Delft and D.Sands, Paragon for practical programming with information-flow control, in: Proceedings of the 11th Asian Symposium on Programming Languages and Systems, Vol. 8301, Springer-Verlag New York, Inc., New York, NY, USA, 2013, pp. 217–232. doi:10.1007/978-3-319-03542-0_16.
11.
N.Broberg and D.Sands, Flow locks: Towards a core calculus for dynamic flow policies, in: Proceedings of the 15th European Conference on Programming Languages and Systems, ESOP’06, Springer-Verlag, Berlin, Heidelberg, 2006, pp. 180–196. doi:10.1007/11693024_13.
12.
N.Broberg and D.Sands, Paralocks: Role-based information flow control and beyond, in: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’10, ACM, New York, NY, USA, 2010, pp. 431–444. doi:10.1145/1706299.1706349.
13.
N.Broberg and D.Sands, Flow locks: Towards a core calculus for dynamic flow policies, Technical report, Chalmers University of Technology and Göteborgs University, May 2006.
14.
N.Broberg, B.van Delft and D.Sands, The anatomy and facets of dynamic policies, in: Proceedings of the 28th IEEE Computer Security Foundations Symposium, 2015, pp. 122–136. doi:10.1109/CSF.2015.16.
15.
S.Chong, Required information release, in: Proceedings of the 23rd IEEE Computer Security Foundations Symposium, IEEE Press, Piscataway, NJ, USA, 2010, pp. 215–227.
16.
S.Chong and A.C.Myers, End-to-end enforcement of erasure and declassification, in: Proceedings of the 21st IEEE Computer Security Foundations Symposium, 2008, pp. 98–111. doi:10.1109/CSF.2008.12.
17.
V.Cortier, S.Kremer and B.Warinschi, A survey of symbolic methods in computational analysis of cryptographic systems, J. Autom. Reason.46(3–4) (2011), 225–259. doi:10.1007/s10817-010-9187-9.
18.
F.Del Tedesco, S.Hunt and D.Sands, A semantic hierarchy for erasure policies, in: Proceedings of the 7th International Conference on Information Systems Security, ICISS’11, Springer-Verlag, Berlin, Heidelberg, 2011, pp. 352–369.
19.
D.E.Denning, A lattice model of secure information flow, Commun. ACM19(5) (1976), 236–243. doi:10.1145/360051.360056.
20.
D.E.Denning and P.J.Denning, Certification of programs for secure information flow, Commun. ACM20(7) (1977), 504–513. doi:10.1145/359636.359712.
21.
D.E.R.Denning, Secure information flow in computer systems., PhD thesis, Purdue University, West Lafayette, IN, USA, 1975.
22.
D.Dolev and A.C.Yao, On the security of public key protocols, Information Theory, IEEE Transactions on29(2) (1983), 198–208. doi:10.1109/TIT.1983.1056650.
23.
E.Elnikety, D.Garg and P.Druschel, SHAI: Enforcing data-specific policies with near-zero runtime overhead, Technical report, Max Planck Institute for Software Systems, Saarland Informatics Campus, Germany, January 2018.
24.
E.Elnikety, A.Mehta, A.Vahldiek-Oberwagner, D.Garg and P.Druschel, Thoth: Comprehensive policy compliance in data retrieval systems, in: Proceedings of the 25th USENIX Conference on Security Symposium, SEC’16, USENIX Association, 2016, pp. 637–654.
25.
C.Fournet and T.Rezk, Cryptographically sound implementations for typed information-flow security, in: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’08, ACM, New York, NY, USA, 2008, pp. 323–335. doi:10.1145/1328438.1328478.
26.
J.A.Goguen and J.Mesegue, Unwinding and inference control, in: Proceedings of the IEEE Symposium on Security and Privacy, 1984, pp. 75–87.
27.
J.A.Goguen and J.Meseguer, Security policies and security models, in: Proceedings of the IEEE Symposium on Security and Privacy, 1982, pp. 11–20.
28.
C.Hammer and G.Snelting, Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs, International Journal of Information Security8(6) (2009), 399–422. doi:10.1007/s10207-009-0086-1.
29.
H.R.Hartson and D.K.Hsiao, Full protection specifications in the semantic model for database protection languages, in: Proceedings of the 1976 Annual Conference, ACM’76, ACM, New York, NY, USA, 1976, pp. 90–95. doi:10.1145/800191.805538.
30.
B.Hicks, D.King, P.McDaniel and M.Hicks, Trusted declassification: High-level policy for a security-typed language, in: Proceedings of the Workshop on Programming Languages and Analysis for Security, PLAS’06, ACM, New York, NY, USA, 2006, pp. 65–74. doi:10.1145/1134744.1134757.
31.
T.H.Hinke, Inference aggregation detection in database management systems, in: Proceedings. 1988 IEEE Symposium on Security and Privacy, 1988, pp. 96–106. doi:10.1109/SECPRI.1988.8101.
32.
A.Johnson, L.Waye, S.Moore and S.Chong, Exploring and enforcing security guarantees via program dependence graphs, in: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI’15, ACM, New York, NY, USA, 2015, pp. 291–302. doi:10.1145/2737924.2737957.
33.
E.Kozyri, Enhancing expressiveness of information flow labels: Reclassification and permissiveness, PhD thesis, Cornell University, Ithaca, New York, USA, 2018, https://search.proquest.com/docview/2167492985?accountid=10267.
34.
E.Kozyri, O.Arden, A.C.Myers and F.B.Schneider, JRIF: Reactive information flow control for Java, Technical report, Cornell Univarsity, February 2016.
35.
M.Krohn, A.Yip, M.Brodsky, N.Cliffer, M.F.Kaashoek, E.Kohler and R.Morris, Information flow control for standard OS abstractions, in: Proceedings of the 21st ACM SIGOPS Symposium on Operating Systems Principles, SOSP’07, ACM, New York, NY, USA, 2007, pp. 321–334. doi:10.1145/1294261.1294293.
36.
P.Laud, Semantics and program analysis of computationally secure information flow, in: Proceedings of the 10th European Symposium on Programming Languages and Systems, ESOP’01, Springer-Verlag, London, UK, 2001, pp. 77–91, http://dl.acm.org/citation.cfm?id=645395.651928. doi:10.1007/3-540-45309-1_6.
37.
P.Laud, On the computational soundness of cryptographically masked flows, in: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’08, ACM, New York, NY, USA, 2008, pp. 337–348. doi:10.1145/1328438.1328479.
38.
P.Laud and V.Vene, A type system for computationally secure information flow, in: Proceedings of the 15th International Conference on Fundamentals of Computation Theory, FCT’05, Springer-Verlag, Berlin, Heidelberg, 2005, pp. 365–377. doi:10.1007/11537311_32.
39.
P.Li and S.Zdancewic, Downgrading policies and relaxed noninterference, in: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’05, ACM, New York, NY, USA, 2005, pp. 158–170. doi:10.1145/1040305.1040319.
40.
P.Li and S.Zdancewic, Practical information-flow control in web-based information systems, in: Proceedings of the 18th IEEE Workshop on Computer Security Foundations, CSFW’05, IEEE Computer Society, Washington, DC, USA, 2005, pp. 2–15. doi:10.1109/CSFW.2005.23.
41.
A.Lux and H.Mantel, Declassification with explicit reference points, in: Computer Security – ESORICS 2009, M.Backes and P.Ning, eds, Springer Berlin Heidelberg, Berlin, Heidelberg, 2009, pp. 69–85. doi:10.1007/978-3-642-04444-1_5.
42.
A.A.Matos and G.Boudol, On declassification and the non-disclosure policy, in: Proceedings of the 18th IEEE Computer Security Foundations Workshop (CSFW’05), 2005, pp. 226–240. doi:10.1109/CSFW.2005.21.
43.
K.Micinski, J.Fetter-Degges, J.Jeon, J.S.Foster and M.R.Clarkson, Checking interaction-based declassification policies for Android using symbolic execution, in: Proceedings of the European Symposium on Research in Computer Security, ESORICS 2015, Springer International Publishing, Cham, 2015, pp. 520–538.
44.
A.C.Myers, JFlow: Practical mostly-static information flow control, in: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’99, ACM, New York, NY, USA, 1999, pp. 228–241. doi:10.1145/292540.292561.
45.
A.C.Myers and B.Liskov, A decentralized model for information flow control, in: Proceedings of the 16th ACM Symposium on Operating Systems Principles, SOSP’97, ACM, New York, NY, USA, 1997, pp. 129–142. doi:10.1145/268998.266669.
46.
A.C.Myers, L.Zheng, S.Zdancewic, S.Chong and N.Nystrom, Jif 3.0: Java information flow, Software release, http://www.cs.cornell.edu/jif, July 2006.
47.
B.P.S.Rocha, S.Bandhakavi, J.den Hartog, W.H.Winsborough and S.Etalle, Towards static flow-based declassification for legacy and untrusted programs, in: Proceedings of the IEEE Symposium on Security and Privacy, 2010, pp. 93–108. doi:10.1109/SP.2010.14.
48.
B.P.S.Rocha, M.Conti, S.Etalle and B.Crispo, Hybrid static-runtime information flow and declassification enforcement, Information Forensics and Security, IEEE Transactions on8(8) (2013), 1294–1305. doi:10.1109/TIFS.2013.2267798.
49.
I.Roy, D.E.Porter, M.D.Bond, K.S.McKinley and E.Witchel, Laminar: Practical fine-grained decentralized information flow control, in: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI’09, ACM, New York, NY, USA, 2009, pp. 63–74. doi:10.1145/1542476.1542484.
50.
A.Sabelfeld and A.C.Myers, Language-based information-flow security, Selected Areas in Communications, IEEE Journal on21(1) (2003), 5–19. doi:10.1109/JSAC.2002.806121.
51.
A.Sabelfeld and A.C.Myers, A model for delimited information release, in: Proceedings of the International Symposium on Software Security (ISSS’03), LNCS, Vol. 3233, Springer-Verlag, 2004, pp. 174–191.
52.
A.Sabelfeld and D.Sands, A per model of secure information flow in sequential programs, in: Proceedings of the 8th European Symposium on Programming Languages and Systems, ESOP’99, Springer-Verlag, Berlin, Heidelberg, 1999, pp. 40–58. doi:10.1007/3-540-49099-X_4.
53.
A.Sabelfeld and D.Sands, Declassification: Dimensions and principles, J. Comput. Secur.17(5) (2009), 517–548, http://dl.acm.org/citation.cfm?id=1662658.1662659. doi:10.3233/JCS-2009-0352.
54.
F.B.Schneider, K.Walsh and E.G.Sirer, Nexus Authorization Logic (NAL): Design rationale and applications, ACM Trans. Inf. Syst. Secur.14(1) (2011), 8:1–8:28. doi:10.1145/1952982.1952990.
55.
G.Smith and R.Alpízar, Secure information flow with random assignment and encryption, in: Proceedings of the 4th ACM Workshop on Formal Methods in Security, FMSE’06, ACM, New York, NY, USA, 2006, pp. 33–44. doi:10.1145/1180337.1180341.
56.
D.Stefan, A.Russo, J.C.Mitchell and D.Mazières, Flexible dynamic information flow control in Haskell, in: Proceedings of the 4th ACM Symposium on Haskell, Haskell’11, ACM, New York, NY, USA, 2011, pp. 95–106. doi:10.1145/2034675.2034688.
57.
R.E.Strom and S.Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Trans. Softw. Eng.12(1) (1986), 157–171. doi:10.1109/TSE.1986.6312929.
58.
D.Volpano, Secure introduction of one-way functions, in: Proceedings of the 13th IEEE Computer Security Foundations Workshop, 2000, pp. 246–254. doi:10.1109/CSFW.2000.856941.
59.
D.Volpano, C.Irvine and G.Smith, A sound type system for secure flow analysis, J. Comput. Secur.4(2–3) (1996), 167–187, http://dl.acm.org/citation.cfm?id=353629.353648. doi:10.3233/JCS-1996-42-304.
60.
D.Volpano and G.Smith, Verifying secrets and relative secrecy, in: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’00, ACM, New York, NY, USA, 2000, pp. 268–276. doi:10.1145/325694.325729.
61.
D.S.Wallach, J.A.Roskind and E.W.Felten, Flexible, extensible Java security using digital signatures, DIMACS Series in Discrete Mathematics and Theoretical Computer Science38 (1996), 59–74. doi:10.1090/dimacs/038/07.
