Abstract
This paper presents a domain specific language, embedded in Haskell (EDSL), for enforcing the information flow policy Delimited Release. To build this language we use Haskell extensions that will allow some kind of dependently-typed programming.
Considering the effort it takes to build a language from scratch, we decided to provide an information-flow security language as an EDSL, using the infrastructure of the host language to support it.
The decision of using Haskell as the implementation language is because it has a powerful type system that makes it possible to encode the security type systems of the embedded language at the type level and also because it is a general purpose language.
The implementation follows an approach where the type of the abstract syntax of the embedded language was decorated with security type information. This way, typed programs will correspond to secure programs, and the verification of the security invariants of programs will be reduced to type-checking.
The embedded security language is designed in a way that is easy to use. We illustrate its use through two examples: an electronic purchase and a secure reading of database information.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Lampson, B. W.: Protection. In: Proceedings of the 5th Princeton Conference on Information Sciences and Systems, Princeton (1971). Reprinted in ACM Operating Systems Review, vol. 8, no. 1, pp 18–24 (1974)
Denning, D.E.: A lattice model of secure information flow. ACM 19(5), 236–243 (1976)
Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 11–20 (1982)
Volpano, D., Smith, G.: A type-based approach to program security. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997. LNCS, vol. 1214, pp. 607–621. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0030629
Myers, A.C., Zheng, L., Zdancewic, S., Chong, S., Nystrom, N.: Jif: java information flow. Software release (2001). http://www.cs.cornell.edu/jif
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_9
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Select. Areas Commun. 21(1), 5–19 (2003)
Myers, A.C., Sabelfeld, A., Zdancewic, S.: Enforcing robust declassification. In: Proceedings of the IEEE Computer Security Foundations Workshop (2004)
Chakravarty, M.M., Keller, G., Jones, S.P., Marlow, S.: Associated types with class. In: POPL (2005)
Russo, A., Claessen, K., Hughes, J.: A library for light-weight information-flow security in Haskell. ACM Sigplan Not. 44(2), 13–24 (2008)
Sabelfeld, A., Sands, D.: Declassification: dimensions and principles. J. Comput. Secur. 17, 517–548 (2009)
Li, P., Zdancewic, S.: Arrows for secure information flow. TCS 411, 1974–1994 (2010)
Yorgey, B.A., Weirich, S., Cretin, J., Peyton Jones, S., Vytiniotis, D., Magalhães, J.P.: Giving Haskell a promotion. In: TLDI (2012)
Eisenberg, R.A., Weirich, S.: Dependently typed programming with singletons. ACM SIGPLAN Not. 47(12), 117–130 (2012)
Löh, A.: Applying type-level and generic programming in Haskell (2015)
Manzino, C., Pardo, A.: Agda formalization of a security-preserving translation from flow-sensitive to flow-insensitive security types. Electron. Notes Theoret. Comput. Sci. 351, 75–94 (2020)
De Latorre, G.: EDSL en Haskell para la programación segura respecto a la propiedad Delimited Release. Final year project. National University of Rosario, Argentina (2022)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Manzino, C., de Latorre, G. (2024). A Haskell-Embedded DSL for Secure Information-Flow. In: Barbosa, H., Zohar, Y. (eds) Formal Methods: Foundations and Applications. SBMF 2023. Lecture Notes in Computer Science, vol 14414. Springer, Cham. https://doi.org/10.1007/978-3-031-49342-3_2
Download citation
DOI: https://doi.org/10.1007/978-3-031-49342-3_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-49341-6
Online ISBN: 978-3-031-49342-3
eBook Packages: Computer ScienceComputer Science (R0)