Abstract
In security-critical software applications, confidential information must be prevented from leaking to unauthorized sinks. Static analysis techniques are widespread to enforce a secure information flow by checking a program after construction. A drawback of these systems is that incomplete programs during construction cannot be checked properly. The user is not guided to a secure program by most systems. We introduce IFbCOO, an approach that guides users incrementally to a secure implementation by using refinement rules. In each refinement step, confidentiality or integrity (or both) is guaranteed alongside the functional correctness of the program, such that insecure programs are declined by construction. In this work, we formalize IFbCOO and prove soundness of the refinement rules. We implement IFbCOO in the tool CorC and conduct a feasibility study by successfully implementing case studies.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
To be precise, it would be a combination of composition and assignment refinements, because an assignment refinement can only introduce one assignment expression.
References
Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)
Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transfer 12(6), 447–466 (2010)
Amtoft, T., Banerjee, A.: Information flow analysis in logical form. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 100–115. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27864-1_10
Amtoft, T., Hatcliff, J., Rodríguez, E.: Specification and checking of software contracts for conditional information flow. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 229–245. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68237-0_17
Andrews, G.R., Reitman, R.P.: An axiomatic approach to information flow in programs. ACM Trans. Program. Langu. Syst. (TOPLAS) 2(1), 56–76 (1980)
Back, R.J.: Invariant based programming: basic approach and teaching experiences. Formal Aspects Comput. 21(3), 227–244 (2009)
Back, R.-J., Eriksson, J., Myreen, M.: Testing and verifying invariant based programs in the SOCOS environment. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 61–78. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73770-4_4
Back, R.J., Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (2012)
Banerjee, A., Naumann, D.A.: Secure information flow and pointer confinement in a Java-like language. In: Computer Security Foundations Workshop, vol. 2, p. 253 (2002)
Barthe, G., Pichardie, D., Rezk, T.: A certified lightweight non-interference Java bytecode verifier. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 125–140. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71316-6_10
Barthe, G., Serpette, B.P.: Partial evaluation and non-interference for object calculi. In: Middeldorp, A., Sato, T. (eds.) FLOPS 1999. LNCS, vol. 1722, pp. 53–67. Springer, Heidelberg (1999). https://doi.org/10.1007/10705424_4
Bordis, T., Cleophas, L., Kittelmann, A., Runge, T., Schaefer, I., Watson, B.W.: Re-CorC-ing KeY: correct-by-construction software development based on KeY. In: Ahrendt, W., Beckert, B., Bubel, R., Johnsen, E.B. (eds.) The Logic of Software. A Tasting Menu of Formal Methods. LNCS, vol. 13360, pp. 80–104. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-08166-8_5
Giannini, P., Servetto, M., Zucca, E., Cone, J.: Flexible recovery of uniqueness and immutability. Theor. Comput. Sci. 764, 145–172 (2019)
Goldberg, A., Robson, D.: Smalltalk-80: The Language and its Implementation. Addison-Wesley Longman Publishing Co., Inc. (1983)
Hall, A., Chapman, R.: Correctness by construction: developing a commercial secure system. IEEE Softw. 19(1), 18–25 (2002)
Hall, R.J.: Fundamental nonmodularity in electronic mail. Autom. Softw. Eng. 12(1), 41–79 (2005)
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. (TOPLAS) 23(3), 396–450 (2001)
Kourie, D.G., Watson, B.W.: The Correctness-by-Construction Approach to Programming. Springer, Heidelberg (2012)
Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall, Hoboken (1994)
Myers, A.C.: JFlow: practical mostly-static information flow control. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 228–241. ACM (1999)
Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for circus. Formal Aspects Comput. 21(1), 3–32 (2009)
Oliveira, M.V.M., Cavalcanti, A., Woodcock, J.: ArcAngel: a tactic language for refinement. Formal Aspects Comput. 15(1), 28–47 (2003)
Oliveira, M.V.M., Gurgel, A.C., Castro, C.G.: CRefine: support for the circus refinement calculus. In: 2008 Sixth IEEE International Conference on Software Engineering and Formal Methods, pp. 281–290. IEEE (2008)
Runge, T., Kittelmann, A., Servetto, M., Potanin, A., Schaefer, I.: Information flow control-by-construction for an object-oriented language using type modifiers (2022). https://arxiv.org/abs/2208.02672
Runge, T., Knüppel, A., Thüm, T., Schaefer, I.: Lattice-based information flow control-by-construction for security-by-design. In: Proceedings of the 8th International Conference on Formal Methods in Software Engineering (2020)
Runge, T., Schaefer, I., Cleophas, L., Thüm, T., Kourie, D., Watson, B.W.: Tool support for correctness-by-construction. In: Hähnle, R., van der Aalst, W. (eds.) FASE 2019. LNCS, vol. 11424, pp. 25–42. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-16722-6_2
Runge, T., Servetto, M., Potanin, A., Schaefer, I.: Immutability and Encapsulation for Sound OO Information Flow Control (2022, under review)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)
Schaefer, I., Runge, T., Knüppel, A., Cleophas, L., Kourie, D., Watson, B.W.: Towards confidentiality-by-construction. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11244, pp. 502–515. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03418-4_30
Strecker, M.: Formal analysis of an information flow type system for MicroJava. Technische Universität München, Technical report (2003)
Sun, Q., Banerjee, A., Naumann, D.A.: Modular and constraint-based information flow inference for an object-oriented language. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 84–99. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27864-1_9
Thüm, T., Schaefer, I., Apel, S., Hentschel, M.: Family-based deductive verification of software product lines. In: Proceedings of the 11th International Conference on Generative Programming and Component Engineering, pp. 11–20 (2012)
Zeyda, F., Oliveira, M., Cavalcanti, A.: Supporting ArcAngel in ProofPower. Electron. Notes Theor. Comput. Sci. 259, 225–243 (2009)
Acknowledgments
This work was supported by KASTEL Security Research Labs.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Runge, T., Kittelmann, A., Servetto, M., Potanin, A., Schaefer, I. (2022). Information Flow Control-by-Construction for an Object-Oriented Language. In: Schlingloff, BH., Chai, M. (eds) Software Engineering and Formal Methods. SEFM 2022. Lecture Notes in Computer Science, vol 13550. Springer, Cham. https://doi.org/10.1007/978-3-031-17108-6_13
Download citation
DOI: https://doi.org/10.1007/978-3-031-17108-6_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-17107-9
Online ISBN: 978-3-031-17108-6
eBook Packages: Computer ScienceComputer Science (R0)