A Method for Model-Driven Information Flow Security

We present a method for software development in which information flow security is taken into consideration from start to finish. Initially, the user of the method (i.e., a software developer) specifies the system architecture and selects a set of security requirements (in the form of secure information flow properties) that the system must adhere to. The user then specifies each component of the system architecture using UML inspired state machines, and refines/transforms these (abstract) state machines into concrete state machines. It is shown that if the abstract specification adheres to the security requirements, then so does the concrete one provided that certain conditions are satisfied.

Quantitative Reasoning About Dependability in Event-B

Formal refinement-based approaches have proved their worth in verifying system correctness. Often, besides ensuring functional correctness, we also need to quantitatively demonstrate that the desired level of dependability is achieved. However, the existing refinement-based frameworks do not provide sufficient support for quantitative reasoning. In this chapter, we show how to use probabilistic model checking to verify probabilistic refinement of Event-B models. Such integration allows us to combine logical reasoning about functional correctness with probabilistic reasoning about reliability.

Security of Dependable Systems

Security and dependability are crucial for designing trustworthy systems. The approach “security as an add-on” is not satisfactory, yet the integration of security in the development process is still an open problem. Especially, a common framework for specifying dependability and security is very much needed. There are many pressing challenges however; here, we address some of them. Firstly, security for dependable systems is a broad concept and traditional view of security, e.g., in terms of confidentiality, integrity and availability, does not suffice. Secondly, a clear definition of security in the dependability context is not agreed upon. Thirdly, security attacks cannot be modeled as a stochastic process, because the adversary’s strategy is often carefully planned. In this chapter, we explore these challenges and provide some directions toward their solutions.

Measuring the Progress of a System Development

For most of the developers and managers, the structure and the behaviour of software systems represented in a graphical manner is more understandable than a formal specification of a system or than plain code. Our previous work combined the intuitiveness of UML with the development rigour brought by formal methods and created progress diagrams. In progress diagrams, the design decisions within a system refinement chain are assisted by the application of patterns and illustrated in a comprehensible and compact manner. In order to rigorously assess and control the design process, we need to thoroughly monitor it. In this chapter we show how the application of generic refinement patterns is reflected in measurements. We establish measures for the evaluation of the design progress of the system, where the progress diagrams are assessed from the size and structural complexity perspective. Our motivation is to support the system developers and managers in making the design decisions that regard the system construction.

Uncertainty Handling in Weighted Dependency Trees

Weighted dependency trees (WDTs) are used in a multitude of approaches to system analysis, such as fault tree analysis or event tree analysis. In fact, any acyclic graph can be transformed to a WDT. Important decisions are often based on WDT analysis. Common for all WDT-based approaches is the inherent uncertainty due to lack or inaccuracy of the input data. In order to indicate credibility of such WDT analysis, uncertainty handling is essential. There is however, to our knowledge, no comprehensive evaluation of the uncertainty handling approaches in the context of the WDTs. This chapter aims to rectify this. We concentrate on approaches applicable for epistemic uncertainty related to empirical input. The existing and the potentially useful approaches are identified through a systematic literature review. The approaches are then outlined and evaluated at a high-level, before a restricted set undergoes a more detailed evaluation based on a set of pre-defined evaluation criteria. We argue that the epistemic uncertainty is better suited for possibilistic uncertainty representations than the probabilistic ones. The results indicate that precision, expressiveness, predictive accuracy, scalability on real-life systems, and comprehensibility are among the properties which differentiate the approaches. The selection of a preferred approach should depend on the degree of need for certain properties relative to others, given the context. The right trade off is particularly important when the input is based on both expert judgments and measurements. The chapter may serve as a roadmap for examining the uncertainty handling approaches, or as a resource for identifying the adequate one.

Application Security for Mobile Devices1

In these last years, mobile devices, such as mobile phones or Personal Digital Assistants, became very popular among people. Moreover, mobile devices became also very powerful, and most of them are also able to execute applications, such as games, Internet browsers, e-mail clients, and so on. Hence, an adequate security support is required on these devices, to avoid that malicious applications damage the device or perform unauthorized accesses to personal data (such as the contact list). This chapter describes the approaches that have been proposed in scientific literature to guarantee the security of mobile devices.

Development of Safety-Critical Control Systems in Event-B Using FMEA

Application of formal methods, in particular Event-B, helps us to verify the correctness of controlling software. However, to guarantee the dependability of software-intensive control systems, we also need to ensure that safety and fault tolerance requirements are adequately represented in a system specification. In this chapter we demonstrate how to integrate the results of safety analysis, in particular failure mode and effect analysis (FMEA), into formal system development in Event-B. The proposed methodology is exemplified by a case study.

Using Model-Driven Risk Analysis in Component-Based Development

Modular system development causes challenges for security and safety as upgraded sub-components may interact with the system in unforeseen ways. Due to their lack of modularity, conventional risk analysis methods are poorly suited to address these challenges. We propose to adjust an existing method for model-based risk analysis into a method for component-based risk analysis. We also propose a stepwise integration of the component-based risk analysis method into a component-based development process. By using the same kinds of description techniques to specify functional behaviour and risks, we may achieve upgrading of risk analysis documentation as an integrated part of component composition and refinement.

Towards a Holistic Approach to Fault Management

Systems with high dependability requirements are increasingly relying on complex on-line fault management systems. Such fault management systems involve a combination of multiple steps – monitoring, data analysis, planning, and execution – that are typically independently developed and optimized. We argue that it is inefficient and ineffective to improve any particular fault management step without taking into account its interactions and dependencies with the rest of the steps. Through six real-life examples, we demonstrate this inefficiency and how it results in systems that either under-perform or are over-budget. We propose a holistic approach to fault management that is aware of all relevant aspects, and explicitly considers the couplings between the different fault management steps. We believe it will produce systems that will better meet cost, performance, and dependability objectives.

Dependability Assessment of Two Network Supported Automotive Applications

The congestion of traffic has been increasingly growing, both in urban areas and in highways. In such a context, the safety of vehicles and their occupants is becoming a real problem. On the other hand, new mobility and wireless communication technologies allow the development of innovative applications to improve traffic safety. This chapter addresses the dependability modelling and evaluation of two such applications supported by communications between the vehicles: automated highway systems and virtual black boxes. Assessment is based on the Stochastic Activity Networks formalism and on a unified modelling approach. We concentrate on the safety of the automated highway and on the availability of the virtual black box data.