Abstract
Cloud computing technologies help developers build scalable distributed apps. Serverless architecture, or Function as a Service (FaaS), which separates app businesses into multiple functions, is one of the cloud-native architectures that has gained popularity. Those functions can be developed and deployed independently without provisioning infrastructure.
Despite the considerable advantages and increasing popularity of cloud-native apps, developers face many challenges when building their cloud-native applications. To ensure the robustness and security of cloud-native apps and protect crucial resources, the design and implementation of functions and associated access control systems play a pivotal role.
In this paper, we have employed formal methods and tools to develop a set of patterns to help cloud-native application developers to design robust serverless apps. We have used Event-B and its associated toolset, Rodin, to construct these formal patterns and demonstrated how these patterns can be used in practical case studies.
The first author is supported by the Turkish National Education Ministry in the U.K. Butler is supported by the HD-Sec project, part of the Digital Security by Design (DSbD) Programme delivered by UKRI to support the DSbD ecosystem.
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
References
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010). https://doi.org/10.1017/CBO9781139195881
Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: A roadmap for the Rodin toolset. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, p. 347. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87603-8_35
Amazon Web Services Inc.: AWS services that work with IAM (2022). https://docs.aws.amazon.com/IAM/latest/UserGuide/reference_aws-services-that-work-with-iam.html
Backes, J., et al.: Semantic-based automated reasoning for AWS access policies using SMT. In: Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018. IEEE (2018). https://doi.org/10.23919/FMCAD.2018.8602994
Butler, M.: Mastering system analysis and design through abstraction and refinement. Eng. Dependable Softw. Syst. (2013). https://doi.org/10.3233/978-1-61499-207-3-49
Butler, M., Fathabadi, A.S., Silva, R.: Event-B and Rodin. In: Industrial Use of Formal Methods: Formal Verification. Wiley-ISTE (2012). https://doi.org/10.1002/9781118561829.ch7
Kanso, A., Youssef, A.: Serverless: beyond the cloud. In: Proceedings of the 2nd International Workshop on Serverless Computing (2017). https://doi.org/10.1145/3154847.3154854
McGrath, G., Brenner, P.R.: Serverless computing: design, implementation, and performance. In: 2017 IEEE 37th International Conference on Distributed Computing Systems Workshops (ICDCSW). IEEE (2017). https://doi.org/10.1109/ICDCSW.2017.36
Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How Amazon web services uses formal methods. Commun. ACM (2015). https://doi.org/10.1145/2699417
Palo Alto Networks: Unit 42 cloud threat report (2020)
Salehi Fathabadi, A., Butler, M., Rezazadeh, A.: Language and tool support for event refinement structures in Event-B. Formal Aspects Comput. https://doi.org/10.1007/s00165-014-0311-1
Synergy Research Group: Huge cloud market still growing at 34% per year; Amazon, Microsoft & Google now account for 65% of the total, April 2022. https://tinyurl.com/yhy7hdwy
Windley, P.: Simplify fine-grained authorization with Amazon verified permissions and Amazon Cognito (2023). https://aws.amazon.com/blogs/security/simplify-fine-grained-authorization-with-amazon-verified-permissionsand-amazon-cognito/
Yagmahan, M.S.N., Rezazadeh, A., Butler, M.: RHP (request handling pattern) and authorization mechanism in Event-B, June 2024. https://doi.org/10.5258/SOTON/D3041
Zahoor, E., Asma, Z., Perrin, O.: A formal approach for the verification of AWS IAM access control policies. In: De Paoli, F., Schulte, S., Broch Johnsen, E. (eds.) ESOCC 2017. LNCS, vol. 10465, pp. 59–74. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67262-5_5
Zahoor, E., Ikram, A., Akhtar, S., Perrin, O.: Authorization policies specification and consistency management within multi-cloud environments. In: Gruschka, N. (ed.) NordSec 2018. LNCS, vol. 11252, pp. 272–288. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03638-6_17
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Ethics declarations
Competing Interests
The author(s) has no competing interests to declare that are relevant to the content of this manuscript.
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Yagmahan, M.S.N., Rezazadeh, A., Butler, M. (2024). An Event-B Formal Model for Access Control and Resource Management of Serverless Apps. In: Bonfanti, S., Gargantini, A., Leuschel, M., Riccobene, E., Scandurra, P. (eds) Rigorous State-Based Methods. ABZ 2024. Lecture Notes in Computer Science, vol 14759. Springer, Cham. https://doi.org/10.1007/978-3-031-63790-2_11
Download citation
DOI: https://doi.org/10.1007/978-3-031-63790-2_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-63789-6
Online ISBN: 978-3-031-63790-2
eBook Packages: Computer ScienceComputer Science (R0)