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

Regular Issues

• AltaRica 3.0 in 10 Modeling Patterns  
  by Michel Batteux, Tatiana Prosvirnova, Antoine Rauzy 
  Abstract: AltaRica 3.0 is an object-oriented modeling language dedicated to probabilistic risk and safety analyses. It is a prominent representative of modeling formalisms supporting the so-called model-based approach in reliability engineering. In this article, we illustrate the key features of the AltaRica~3.0 technology by presenting the implementation of ten very common modeling patterns. We demonstrate in this way the expressive power of the language as well as its elegance and simplicity of use.
  Keywords: Probabilistic risk and safety assessmentrnmodeling languagesrnmodeling patternsrnAltaRica 3.0.
  
  
• Iterative integration of TTEthernet network flows  
  by Sofiene Beji, Sardaouna Hamadou, John Mullins, Abdelouahed Gherbi 
  Abstract: TTEthernet has been proposed as an improvement of the Ethernet network protocol to ensure communication of critical systems. Some of these systems, such as avionics systems, are complex and evolving ones. Therefore, they are designed iteratively by integrating in each iteration some components of the system. Adding new functionalities may induce substantial additional costs of reconfiguration of the system in order to meet the real-time requirements. Based on the constraint programming techniques, we develop in this paper a cost optimization approach that meets the TTEthernet specification and validates the latencies requirements in an accurate way. We illustrate our approach on a case study with the MiniZinc tool (Nethercote et al. , 2007).
  Keywords: TTEthernet; Iterative Integration; Scheduling; Real-Time Systems.
  
  

Special Issue on: S4CIP'17 Methods and Tools for Assurance of Critical Infrastructure Protection

• Survey on international standards and best practices for patch management of complex Industrial Control Systems: the critical infrastructure of particle accelerators case study  
  by Ugo Gentile, Luigi Serio 
  Abstract: Industrial Control Systems (ICSs) are control and data acquisition systems employed to control distributed assets with a centralised data acquisition and supervisory control. ICSs strictly rely on computer-based systems and on installed remote controllers, which are subject to a constant patch deployment to upgrade functionalities, to resolve security issues and to reduce potential flaws. The patch management is not a trivial process since it can introduce new vulnerabilities within the systems. A key factor to perform successful patch management is to comply with the recommendations provided by the international standards and by the best practices currently adopted in the industry. This paper surveys the few existing international standards on patch management and the best practices, currently adopted in industry, and evaluates the relevance of standards and the best practices to the context of critical infrastructures for particle accelerators.
  Keywords: Industrial Control Systems; Patch management; Critical Infrastructure; Particles accelerators.
  
  
• A methodology for assuring the safety and security of critical infrastructure based on STPA and Event-B  
  by Giles Howard, Michael Butler, Vladimiro Sassone, John Colley 
  Abstract: Cyber-physical systems represent a challenge to conventional security and safety analysis techniques due to their complexity and the need to consider both safety and security equally. It is also important that the requirements generated to mitigate against safety and security risks are clear and adequately address the underlying issue. A methodology is presented in this paper to allow for integrated safety and security analysis of cyber-physical systems, particularly in a critical infrastructure context. This methodology uses a modified form of STPA, which has been coupled with our concept of adversarial modelling, to analyse for security and safety hazards which are then mitigated against by the creation of critical requirements. These critical requirements are then validated through their application to an Event-B formal model, allowing for their completeness to be verified. The output of the methodology is a set of critical requirements that guide iteration of and improvements to the system design to ensure its safety and security are maintained.
  Keywords: Systems Theoretic Process Analysis; hazard analysis; Event-B; safety analysis; security analysis; critical infrastructure; cyber-physical systems; adversarial modelling; critical systems.
  
  

Special Issue on: Methods and Tools for Assurance of Critical Infrastructure Protection

• A Versatile Approach for ranking and modelling of Non Functional Requirements  
  by Harsimran Kaur 
  Abstract: RTo effectively encode domain knowledge of customers and implementation strategies of developers in Critical Computer Based System (CBS), Requirement Engineering plays a very significant role. For development of quality software for CBS, it is indeed necessary to specify both Functional and Non-Functional Requirements (NFRs) for the proposed software. However, unlike functional requirements, NFRs are not given much importance and are often generically captured which results in missing out on quality parameters during CBS development. This lacuna can be taken care with inclusion of details regarding NFRs for the proposed softwares at initial stages of CBS development. On the other hand subjective nature and complex common connections amongst the NFRs makes it quite unrealistic to concentrate on each of the NFR. This complexity can be addressed by use of Interpretive Structural Modelling (ISM) and Analytical Hierarchy Process (AHP) methods for identification of critical NFRs. Further, new artifacts have been introduced in Use Case Diagram and Reference Model to document and validate the identified critical NFRs. The proposed work determines the degree of mutual reliance between NFRs so that software analysts can figure out all the concerns related to NFRs during the underlying periods of programming advancement. Credibility of proposed work, each proposed artifact in Software Requirement Specification (SRS) document was initially analyzed individually and then later on was compared with other built up and noticeable methodologies. By use of cognitive dimension analysis and complexity measures it was established that the proposed artifact not only treats NFRs informally and formally but also make them viable, traceable and visible to different classes of users for analysis.
  Keywords: Non-Functional Requirements (NFR); Software Requirement Specification (SRS); Use Case; Reference Model; Interpretive Structural Modelling; Formal Modelling.
  
  
• Formal Methods in Dynamic Software Updating: A survey  
  by Razika Lounas, Mohamed Mezghiche, Jean-Louis Lanet 
  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 categorize 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.
  Keywords: Dynamic software updating; formal methods; correctness criteria; critical systems; systems safety.
  
  
• A Fully Encrypted High-Speed Microprocessor Architecture: The Secret Computer in Simulation  
  by Peter Breuer, Jonathan Bowen 
  Abstract: The architecture of an encrypted high performance microprocessor designed on the principle that a nonstandard arithmetic generates encrypted processor states is described here. Data in registers, in memory and on buses exists in encrypted form. Any block encryption is admissible in the architecture.rnrnAn encrypted version of the standard OpenRISC instruction set is understood by the processor. It is proved here, for programs written in a minimal subset of instructions, that the platform is secure against `Iago' attacks, in that the privileged operator or a subverted operating system cannot decrypt the program output, nor change the program's output to any designated value.rnrnPerformance measures from cycle-accurate behavioural simulation of the platform are given for 64-bit RC2 (symmetric, keyed) and 72-bit Paillier (asymmetric, additively homomorphic, no key in-processor) encryptions. Measurements are centred on a nominal 1GHz clock with 3ns cache and 15ns memory latency, which is conservative with respect to available technology.
  Keywords: Computer Security; Encrypted Computation.