Formal methods in dynamic software updating: a survey
Abstract
Dymanic software updating DSU consists in updating running programs on-the-fly without any downtime that leads to systems unavailability. The use of DSU in critical applications raises several issues related to update correctness. Indeed, an erroneous dynamic update may introduce safety vulnerabilities and security breaches. In this perspective, the use of formal methods has gained a large interest since they respond to the high need of rigor required by such applications. Several frameworks were developed to first express update correctness which is based on several criteria. Then, the proposed formalisms are used to specify DSU systems, express correctness criteria and establish them. In this paper, we present a review of researches on the application of formal methods to DSU systems. We give a classification of systems according to the paradigms of programming languages and then we explain the correctness criteria and categorise the articles regarding the approaches of formalisation to establish the correctness. This information is useful to help ongoing researches in having an overview on the application of formal methods in DSU.
References
[1]
Altekar, G., Bagrak, I., Burstein, P. and Schultz, A. (2005) 'OPUS: online patches and updates for security', Proceedings of the 14th Conference on USENIX Security Symposium, USENIX Association, Vol. 14.
[2]
An, S., Ma, X., Cao, C., Yu, P. and Xu, C. (2015) 'An event-based formal framework for dynamic software update', IEEE International Conference on Software Quality, Reliability and Security, QRS, Vancouver, BC, Canada.
[3]
Anderson, A. and Rathke, J. (2009) 'Migrating protocols in multi-threaded message-passing systems', Proceedings of the 2nd International Workshop on Hot Topics in Software Upgrades (HotSWUp).
[4]
Anderson, G. (2013) Behavioural Properties and Dynamic Software Update for Concurrent Programs, PhD thesis, University of Southampton.
[5]
Anderson, G. and Rathke, J. (2012) 'Dynamic software update for message passing programs', Programming Languages and Systems, Springer Berlin Heidelberg, pp.207-222.
[6]
ANSSI (Secrétariat Général de la Défense et de la Sécurité Nationale Security) (2015) Requirements for Post-Delivery Code Loading, National Agency of Information Systems Security, Paris, France.
[7]
Arnold, J. and Frans, K.M. (2009) 'Ksplice: automatic rebootless kernel updates', Proceedings of the 4th ACM European Conference on Computer Systems (EuroSys), pp.187-198.
[8]
Baier, C. and Katoen, J.P. (2008) Principles of Model Checking (Representation and Mind Series), The MIT Press, Cambridge, Massachusetts; London, England.
[9]
Baumann, A., Kerr, J., Da Silva, D., Krieger, O. and Wisniewski, R.W. (2005) 'Module hot-swapping for dynamic update and reconfiguration in K42', in 6th Linux Conf. Au.
[10]
Bertot, Y. and Castéran, P. (2013) Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, Springer Science & Business Media.
[11]
Bierman, G., Hicks, M., Sewell, P. and Stoyle, G. (2003) 'Formalizing dynamic software updating', On-line Proceedings of the Second International Workshop on Unanticipated Software Evolution (USE).
[12]
Boyapati, C., Liskov, B., Shrira, L., Moh, C-H. and Richman, S. (2003) 'Lazy modular upgrades in persistent object stores', Proceedings of the 18th Annual ACM SIGPLAN Conference on Object-oriented Programing, Systems, Languages, and Applications, ACM publisher.
[13]
Buisson, J. and Dagnat, F. (2010) 'ReCaml: Execution state as the cornerstone of reconfigurations', SIGPLAN Not., ACM, New York, pp.27-38.
[14]
Buisson, J., Dagnat, F., Leroux, E. and Martinez, S. (2016) 'Safe reconfiguration of Coqcots and Pycots components', Journal of Systems and Software, Vol. 122, No. C, pp.430-444.
[15]
Charlton, N., Horsfall, B. and Reus, B. (2011) 'Formal reasoning about runtime code update', in ICDE Workshops, pp.134-138.
[16]
Chen, H., Yu, J., Chen, R., Zang, B. and Yew, P-C. (2007) 'POLUS: a powerful live updating system', Proceedings of the 29th International Conference on Software Engineering (ICSE), pp.271-281.
[17]
Chen, J. and Huang, L. (2009) 'Dynamic service update based on OSGi', Software Engineering, (WCSE), WRI World Congress, pp.493-497.
[18]
Chen, J., Huang, L., Du, S. and Zhou, W. (2010) 'A formal model for supporting frameworks of dynamic service update based on OSGi', in 17th Asia Pacific Software Engineering Conference (APSEC), pp.234-241.
[19]
Common Criteria (2016) [online] http://www.commmoncriteria.org (accessed 15th October 2017).
[20]
de Pina, L., Veiga, L. and Hicks, M. (2014) 'Rubah: DSU for java on a stock JVM', Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA'14, ACM New York, NY, USA, October, Vol. 49, No. 10, pp.103-119.
[21]
de Pina, L.G.G. (2016) Practical Dynamic Software Updating, PhD thesis, University of Lisbon, Portugal.
[22]
Dershowitz, N. and Jouannaud, J.P. (1990) 'Rewrite systems', Handbook of Theoretical Computer Science, Vol. B, pp.243-320, MIT Press, Cambridge, MA, USA.
[23]
Dmitriev, M. (2001) 'Towards flexible and safe technology for runtime evolution of java language applications', in Proceedings of the Workshop on Engineering Complex Object-Oriented Systems for Evolution.
Index Terms
- Formal methods in dynamic software updating: a survey
Recommendations
An Algebraic Approach to Formal Analysis of Dynamic Software Updating Mechanisms
APSEC '12: Proceedings of the 2012 19th Asia-Pacific Software Engineering Conference - Volume 01Dynamic Software Updating (DSU) is a promising software maintenance technique, which aims at updating running software systems on the fly without incurring any downtime. The systems that require dynamic updating usually require high reliability ...
An Approach to Dynamic Software Updating for Java
PACIIA '08: Proceedings of the 2008 IEEE Pacific-Asia Workshop on Computational Intelligence and Industrial Application - Volume 02To cope with demands for new and extended functionality, software systems must be updated regularly. Some applications, however, need to be continuously available because they are providing services that are important for users at all times. To avoid ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Publisher
Inderscience Publishers
Geneva 15, Switzerland
Publication History
Published: 25 May 2019
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 20 Nov 2024
Other Metrics
Citations
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in