Abstract
Security of software systems has to be preserved while they grow and change incrementally. The problem is to make the analysis of their security properties adhere to such a development. In particular we concentrate here on static type systems. Given a non-incremental type system, the algorithm we propose permits using it incrementally, so avoiding to develop new incremental versions of it. As a proof-of-concept we show how our technique permits an incremental checking of non-interference with robust declassification, starting from the classical type system by Myers, Sabelfeld and Zdancewic.
The first two authors have been partially supported by U. Pisa project PRA_2018_66 DECLware: Declarative methodologies for designing and deploying applications. The last author is supported by IMT project PAI VeriOSS.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abadi, M.: Secrecy by typing in security protocols. In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol. 1281, pp. 611–638. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0014571
Abadi, M.: Secrecy by typing in security protocols. J. ACM 46(5), 749–786 (1999)
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Local policies for resource usage analysis. ACM Trans. Program. Lang. Syst. 31(6), 23:1–23:43 (2009)
Busi, M., Degano, P., Galletta, L.: Using standard typing algorithms incrementally. In: 11th NASA Formal Methods, Proceedings. To appear in LNCS. Springer (2019). https://arxiv.org/abs/1808.00225
Calcagno, C., et al.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3–11. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9_1
Flanagan, C., Abadi, M.: Types for safe locking. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 91–108. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49099-X_7
Grossman, D., Morrisett, G., Jim, T., Hicks, M., Wang, Y., Cheney, J.: Region-based memory management in cyclone. SIGPLAN Not. 37(5), 282–293 (2002). https://doi.org/10.1145/543552.512563
Harman, M., O’Hearn, P.: From start-ups to scale-ups: opportunities and open problems for static and dynamic program analysis. In: IEEE International Working Conference on Source Code Analysis and Manipulation (2018)
Higuchi, T., Ohori, A.: A static type system for JVM access control. ACM Trans. Program. Lang. Syst. 29(1), 4 (2007)
Leroy, X., Pessaux, F.: Type-based analysis of uncaught exceptions. ACM Trans. Program. Lang. Syst. 22(2), 340–377 (2000)
Meadows, C.A.: Formal methods for cryptographic protocol analysis: emerging issues and trends. IEEE J. Sel. Areas Commun. 21(1), 44–54 (2003)
Myers, A.C., Sabelfeld, A., Zdancewic, S.: Enforcing robust declassification and qualified robustness. J. Comput. Secur. 14(2), 157–196 (2006)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003). https://doi.org/10.1109/JSAC.2002.806121
Smith, G.: Principles of secure information flow analysis. In: Christodorescu, M., Jha, S., Maughan, D., Song, D., Wang, C. (eds.) Malware Detection, pp. 291–307. Springer, Boston (2007). https://doi.org/10.1007/978-0-387-44599-1_13
Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2/3), 167–188 (1996)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Busi, M., Degano, P., Galletta, L. (2019). Robust Declassification by Incremental Typing. In: Guttman, J., Landwehr, C., Meseguer, J., Pavlovic, D. (eds) Foundations of Security, Protocols, and Equational Reasoning. Lecture Notes in Computer Science(), vol 11565. Springer, Cham. https://doi.org/10.1007/978-3-030-19052-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-19052-1_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-19051-4
Online ISBN: 978-3-030-19052-1
eBook Packages: Computer ScienceComputer Science (R0)