Title: Petri net-based verification of security protocol implementation in software evolution

Authors: Mohd Anuaruddin Bin Ahmadon; Shingo Yamaguchi; B.B. Gupta

Addresses: Graduate School of Science and Engineering, Yamaguchi University, Ube, Yamaguchi Pref., 755-8611, Japan ' Graduate School of Science and Engineering, Yamaguchi University, Ube, Yamaguchi Pref., 755-8611, Japan ' Department of Computer Engineering, National Institute of Technology Kurukshetra, Kurukshetra, 136119, Haryana, India

Abstract: Implementation of security protocol in software plays an important role to protect the whole system from vulnerabilities. In order to protect the system from new threats, software needs to adapt to new security requirements thus security upgrades and patches are implemented to the software. Previous works only focus on logical correctness of the security protocol but we focus on the successful implementation of security protocol in a program. A program evolves as programmers apply security patches to its source code. Hence, the process of verifying important security protocol implementation is difficult. In this paper, we propose model-driven security verification throughout software evolution. It consists of two major methods: 1) reverse engineering method to translate a program into Petri net model; 2) model-driven verification method to confirm that the security protocol implementation is valid. Concretely, for a program X that implements a security protocol specification A, does its derivation Y also implement A? The answer is yes if Y inherits the behaviour of X. We apply behavioural inheritance analysis to verify security protocol implementation. We also illustrate the methods with an example in software evolution.

Keywords: software evolution; reverse engineering; security protocol; Petri net; behavioural inheritance.

DOI: 10.1504/IJES.2018.095754

International Journal of Embedded Systems, 2018 Vol.10 No.6, pp.503 - 517

Received: 21 Jul 2016
Accepted: 09 Dec 2016
Published online: 22 Oct 2018 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article