International Journal of Critical Computer-Based Systems (6 papers in press)

Regular Issues

• Towards a Hybrid Formal Analysis Technique for Safety-Critical Software Architectures  
  by Ammar Boucherit, Laura M. Castro, Hasan Osman, Khababa Abdallah 
  Abstract: Given the catastrophic damage that bugs in critical systems can inflict on human life and its socio-economic environment, the use of rigorous analysis techniques while developing such systems is getting more and more important especially with the increasingly growing complexity of their architecture.rnHowever, the aforementioned growing complexity of such systems architecture leads to many scalability issues for the existing formal specification and verification approaches.rnThis paper presents a novel and scalable formal development approach for critical system software architectures. In particular, our proposal is based on rewriting logic and combines both model checking and property-based testing techniques to bridge the gap between these complementary techniques, and hence overcome the drawbacks of previous attempts to ensure the absence of undesired or unexpected behavior in the specification and implementation of a critical system.
  Keywords: Rewriting Logic; Maude; Property-Based Testing; Software architecture; Critical systems.
  
  
• Towards Compositional Verification of Synchronous Reactive Systems  
  by Sarah Chabane, Rabéa Ameur-Boulifa, Mohamed Mezghiche 
  Abstract: We present work towards a compositional design approach that will lead designers to develop safe reactive systems. To this end, we extend the theory of I/O-automata that is widely used for modelling reactive systems with composition operator required for dealing with a specific assembly of such systems: systems that consist of a chain of components arranged so that the output of each component is the input of the next, and behave like pipelines. We show that the proposed composition operator ensures semantics preserving of reactive components models. The paper presents a general result on correct-by-construction approach for reactive systems design.
  Keywords: Rigorous system design; component-based design ;formal verification; correctness-by-construction.
  
  
• An SMT-Based Approach for Generating Trace Examples and Counter-examples of Parametric Properties  
  by Salim Chehida, Yves Ledru, Yoann Blein, German Vega 
  Abstract: The ParTraP language has been designed to express temporal and timed properties on finite execution traces of parametric events. It aims to ease properties expression for users not experienced in formal methods. In this paper, we propose an approach that allows generating trace examples and counterexamples in an understandable fashion in order to help such users to better express requirements. So, ParTraP properties are mapped into a SMT (Satisfiability Modulo Theories) context to be fed to Z3 SMT solver to check satisfaction and produce interpretations. A tool named ParTraP-EG is dedicated to that purpose. We report experiments carried out on a set of properties from an industrial case study of computer-aided surgery system.
  Keywords: Runtime Verification; Parametric Traces; Temporal and Timed Properties; Satisfiability Modulo Theories; Trace Examples and Counter-examples.
  
  
• Deep learning models for multi-class malware classification using Windows exe API Calls  
  by Kakelli Anil Kumar, Kaustubh Kumar, Nag Lohith Chiluka 
  Abstract: Metamorphic malware is new and one of the most advanced malwares recently discovered. This malware can bypass anti-viruses and are much harder to detect if present in any computer system or network. This research paper intends to develop a better classification method for this metamorphic malware using the latest malware API calls dataset. The multi-class malware classification used in this study is Gated Recurrent Units (GRU). Another non-conventional multi-class malware classification method used is Convolution Neural Network with Long Short-Term Memory (CNN+LSTM). The multi-classification results obtained by GRU are 55% with a 0.56 F1-score, and CNN+LSTM is 60% with a 0.61 F1-score, which is quite good. Moreover, the performance of the proposed deep learning models is compared against different classifiers and existing models to show their effectiveness in categorizing malware.
  Keywords: Metamorphic Malware; GRU; CNN+LSTM.
  
  
• Abstract Executions of Stochastic Discrete Event Systems  
  by Michel Batteux, Tatiana Prosvirnova, Antoine Rauzy 
  Abstract: Stochastic discrete event systems play a steadily increasing role in reliability engineering and beyond in systems engineering. Designing stochastic discrete event systems presents however a well-known difficulty: models are hard to debug and to validate because of the existence of infinitely many possible executions, itself due to stochastic delays, which are possibly intertwined with deterministic ones. In this article, revisiting ideas introduced in the framework of model-checking of timed and hybrid systems, we show that it is possible to abstract the time in stochastic discrete event systems, therefore alleviating considerably debugging and validation tasks. More specifically, we show that schedules of transitions can be abstracted into systems of linear inequalities and that abstract and concrete executions are bisimilar: any concrete execution can be simulated by an abstract execution and reciprocally any abstract execution corresponds to at least one concrete execution. Moreover, we propose an efficient algorithm to determine whether generated systems of linear inequalities have solutions. This algorithm takes advantage of the very specific form of inequalities. The result presented in this article represents thus a very important step forward in quality assurance of stochastic models of complex technical systems. We illustrate the potential of the proposed approach by means of AltaRica 3.0 models.
  Keywords: Stochastic Discrete Event Systems; Timed and Hybrid Automata; Abstract Intepretation; AltaRica 3.0;.
  
  
• Formal Modelling and Verification of High Interactive Honeypot using Coloured Petri Nets  
  by Sheetal Gokhale, Irfan Siddavatam, Ashwini Dalvi, Mohammed Shaikh, Suchitra Patil 
  Abstract: Honeypot is an active defense mechanism intended to mimic a computer system concealing its identity to misguide attackers. The mechanism traps an attacker and collects intrusion information as they trespass a network environment and cause a menace for their interest. The paper proposes a honeypot tool with deadlock and livelock states to strengthen the defence mechanism and engage the attacker for a longer period. The proposed work aims to present the formal analysis of a honeypot using coloured petri nets tool. The three core components of the honeypot, such as data capture, control and collection, are included in the formal modelling to study the behavioural properties of a honeypot in a deadlock and livelock state. The main objective is to emphasize the working of high interaction honeypot in deadlock or livelock states under an attack surface. The honeypots formal model verification using a state-space tool in coloured petri net determines that an attacker wedged in a deadlock or livelock state fails to navigate further to fulfil malicious intent, thereby deceiving an attacker for a longer period.
  Keywords: honeypot; coloured petri net; CPN; formal analysis; cowrie.