Abstract Deep neural networks (DNNs) are key components for the implementation of autonomy in systems that operate in highly complex and unpredictable environments (self-driving cars, smart traffic systems, smart manufacturing, etc.). It is well known that DNNs are vulnerable to adversarial examples, i.e. minimal and usually imperceptible perturbations, applied to their inputs, leading to false predictions. This threat poses critical challenges, especially when DNNs are deployed in safety or security-critical systems, and renders as urgent the need for defences that can improve the trustworthiness of DNN functions. Adversarial training has proven effective in improving the robustness of DNNs against a wide range of adversarial perturbations. However, a general framework for adversarial defences is needed that will extend beyond a single-dimensional assessment of robustness improvement; it is essential to consider simultaneously several distance metrics and adversarial attack strategies. Using such an approach we report the results from extensive experimentation on adversarial defence methods that could improve DNNs resilience to adversarial threats. We wrap up by introducing a general adversarial training methodology, which, according to our experimental results, opens prospects for an holistic defence against a range of diverse types of adversarial perturbations.

Abstract Full a posteriori verification of the correctness of modern software systems is practically infeasible due to the sheer complexity resulting from their intrinsic concurrent nature. An alternative approach consists of ensuring correctness by construction. We discuss the Rigorous System Design (RSD) approach, which relies on a sequence of semantics-preserving transformations to obtain an implementation of the system from a high-level model while preserving all the properties established along the way. In particular, we highlight some of the key requirements for the feasibility of such an approach, namely availability of (1) methods and tools for the design of correct-by-construction high-level models and (2) definition and proof of the validity of suitable domain-specific abstractions. We summarise the results of the extended versions of seven papers selected among those presented at the $$1\mathrm {st}$$ 1 st and the $$2\mathrm {nd}$$ 2 nd International Workshops on Methods and Tools for Rigorous System Design (MeTRiD 2018–2019), indicating how they contribute to the advancement of the RSD approach.

A formal semantics is introduced for a Process Network model, which combines streaming and reactive control processing with task parallelism properties suitable to exploit multi-cores. Applications that react to environment stimuli are implemented by communicating sporadic and periodic tasks, programmed independently from an execution platform. Two functionally equivalent semantics are defined, one for sequential execution and one real-time. The former ensures functional determinism by implying precedence constraints between jobs (task executions), hence, the program outputs are independent from the task scheduling. The latter specifies concurrent execution on a real-time platform, guaranteeing all model’s constraints; it has been implemented in an executable formal specification language. The model’s implementation runs on multi-core embedded systems, and supports integration of run-time managers for shared HW/SW resources (e.g. for controlling QoS, resource interference or power consumption). Finally, a model transformation approach has been developed, which allowed to port and statically schedule a real spacecraft on-board application on an industrial multi-core platform.

Summary The design of software for networked systems with nodes running an Internet of things operating system faces important challenges due to the heterogeneity of interacting things and the constraints stemming from the often limited amount of available resources. In this context, it is hard to build confidence that a design solution fulfills the application's requirements. This paper introduces a design flow for web service applications of the representational state transfer style that is based on a formal modeling language, the behaviour, interaction, priority (BIP) component framework. The proposed flow applies the principles of separation of concerns in a component‐based design process that supports the modular design and reuse of model artifacts. The BIP tools for state‐space exploration allow verifying qualitative properties for service responsiveness, ie, the timely handling of events. Moreover, essential quantitative properties are validated through statistical model checking of a stochastic BIP model. All properties are preserved in actual implementation by ensuring that the deployed code is consistent with the validated model. We illustrate the design of a representational state transfer sense‐compute‐control application for a Wireless Personal Area Network architecture with nodes running the Contiki operating system. The results validate qualitative and quantitative properties for the system and include the study of error behaviours.

Context: Modern automated source code analysis techniques can be very successful in detecting a priori de- fined defect patterns and security vulnerabilities. Yet, they cannot detect flaws that manifest due to erroneous translation of the software’s functional requirements into the source code. The automated detection of logical errors that are attributed to a faulty implementation of applications’ functionality, is a relatively uncharted territory. In previous research, we proposed a combination of automated analyses for logical error detection. In this paper, we develop a novel business-logic oriented method able to filter mathematical depictions of software logic in order to augment logical error detection, eliminate previous limitations in analysis and provide a formal tested logical error detection classification without subjective discrepancies. As a proof of concept, our method has been implemented in a prototype tool called PLATO that can detect various types of logical errors. Potential logical errors are thus detected that are ranked using a fuzzy logic system with two scales characterizing their impact: (i) a Severity scale, based on the execution paths’ characteristics and Information Gain, (ii) a Reliability scale, based on the measured program’s Computational Density. The method’s effectiveness is shown using diverse experiments. Albeit not without restrictions, the proposed automated analysis seems able to detect a wide variety of logical errors, while at the same time limiting the false positives.

The focus of this work is the on-demand resource provisioning in cloud computing, which is commonly referredto as cloud elasticity. Although a lot of effort has been invested in developing systems and mechanisms that enable elasticity, the elasticity decision policies tend to be designed without quantifying or guaranteeing the quality of their operation. We present an approach towards the development of more formalized and dependable elasticity policies. We make two distinct contributions. First, we propose an extensible approach to enforcing elasticity through the dynamic instantiation and online quantitative verification of Markov Decision Processes(MDP) using probabilistic model checking. Second, various concrete elasticity models and elasticity policies are studied. We evaluate the decision policies using traces from a realNoSQL database cluster under constantly evolving externalload. We reason about the behaviour of different modelling and elasticity policy options and we show that our proposal can improve upon the state-of-the-art in significantly decreasing under-provisioning while avoiding over-provisioning.

Abstract: Recent advances in static and dynamic program analysis resulted in tools capable to detect various types of security bugs in the Applications under Test (AUTs). However, any such analysis is designed for a priori specified types of bugs and it is characterized by some rate of false positives or even false negatives and certain scalability limitations. We present a new analysis and source code classification technique, and a pro-totype tool aiming to aid code reviews in the detection of general information flow dependent bugs. Our approach is based on classifying the criticality of likely exploits in the source code using two measuring functions, namely Severity and Vulnerability. For an AUT, we analyse every single pair of input vector and program sink in an execution path, which we call an Information Block (IB). A classification technique is introduced for quantifying the Severity (danger level) of an IB by static analysis and computation of its En-tropy Loss. An IB’s Vulnerability is quantified using a tainted object propagation analysis along with a Fuzzy Logic system. Possible exploits are then characterized with respect to their Risk by combining the computed Severity and Vulnerability measurements through an aggregation operation over two fuzzy sets. An IB is characterized of a high risk, when both its Severity and Vulnerability rankings have been found to be above the low zone. In this case, a detected code exploit is reported by our prototype tool, called Entroine. The effectiveness of our approach has been tested by analysing 45 Java programs of NIST’s Juliet Test Suite, which implement three different common weakness exploits. All existing code exploits were detected without any false positive. 1

Behavioral correctness of service compositions refers to the absence of service interaction flaws, so that essential service properties like deadlock freedom are preserved and correctness properties related to safety and liveness are assured. Model checking is a widespread technique and it is based on extracting an abstract model representation of the program defining a service orchestration or choreography. During model extraction, the original structure of the service composition cannot be preserved and backwards traceability of the verification findings is not possible. We propose a rigorous analysis within the BIP component framework. Being rigorous means that the analyst is able to reason on which properties hold and why. The BIP language offers a sound execution semantics for a minimal set of primitives and constructs for modeling and composing layered components. We formally define the WS-BPEL 2.0 execution semantics and we provide a structure-preserving translation (embedding) of WS-BPEL to BIP. Structure preservation is feasible, due to the formally grounded expressiveness properties of BIP. As a proof of concept, we apply the developed embedding to a sample BPEL program and present the analysis results for a safety property. By exploiting the BIP model structure we interpret the analysis findings in terms of the service interactions stated in the BPEL source code. A significant benefit of BIP is that it applies compositional reasoning on the model structure to guarantee essential correctness properties and avoid, as much as possible, the scalability limitations of conventional model checking.

SUMMARY In modern transaction processing software, the ACID properties (atomicity, consistency, isolation, durability) are often relaxed, in order to address requirements that arise in computing environments of today. Typical examples are the long‐running transactions in mobile computing, in service‐oriented architectures and B2B collaborative applications. These new transaction models are collectively known as advanced or extended transactions. Formal specification and reasoning for transaction properties have been limited to proof‐theoretic approaches, despite the recent progress in model checking. In this work, we present a model‐driven approach for generating a provably correct implementation of the transaction model of interest. The model is specified by state machines for the transaction participants, which are synchronized on a set of events. All possible execution paths of the synchronized state machines are checked for property violations. An implementation for the verified transaction model is then automatically generated. To demonstrate the approach, the specification of nested transactions is verified, because it is the basis for many advanced transaction models. Concurrency and Computation: Practice and Experience. Copyright © 2012 John Wiley & Sons, Ltd.

In this paper we present an approach for investigating the feasibility of reducing inference control to access control, as the latter is a more desirable means of preventing unauthorized access to sensitive data. Access control is preferable over inference control in terms of efficiency, but it fails to offer confidentiality in the presence of inference channels. We argue that during the design phase of a data schema and the definition of user roles, inference channels should be considered. An approach is introduced that can be integrated into a risk assessment exercise to assist in determining the roles and/or attributes that lower the risks associated with information disclosure from inference. The residual risk from the remaining inference channels could be treated by well known inference control mechanisms.

The current proliferation of mobile devices has resulted in a large diversity of hardware specifications, each designed for different services and applications (e.g. cell phones, smart phones, PDAs). At the same time, e-mail message delivery has become a vital part of everyday communications. This article provides a cost-aware study of an RSA-based e-mail protocol executed upon the widely used Apple iPhone 1,2 with ARM1176JZF-S, operating in an High Speed Downlink Packet Access (HSDPA) mobile environment. The proposed study employs formal analysis techniques, such as probabilistic model checking, and proceeds to a quantitative analysis of the email protocol, taking into account computational parameters derived by the devices' specifications. The value of this study is to form a computer-aided framework which balances the tradeoff between gaining in security, using high-length RSA keys, and conserving CPU resources, due to hardware limitations of mobile devices. To the best of our knowledge, this is the first time that probabilistic model checking is utilized towards verifying a secure e-mail protocol under hardware constrains. In fact, the proposed analysis can be widely exploited by protocol designers in order to verify their products in conjunction with specific mobile devices.

Abstract Model checking cryptographic protocols have evolved to a valuable method for discovering counterintuitive security flaws, which makes it possible for a hostile agent to subvert the goals of the protocol. Published works and existing security analysis tools are usually based on general intruder models that embody at least some aspects of the seminal work of Dolev–Yao, in an attempt to detect failures of secrecy. In this work, we propose an alternative intruder model, which is based on a thorough analysis of how potential attacks might proceed. We introduce an intruder model that provides an open‐ended base for the integration of multiple basic attack tactics. Those attack tactics have the possibility to be combined, in a way to compose complex attack actions that require a number of procedural steps from the intruder's side, such as a Denial of Service attack. In our model checking approach, protocol correctness is checked by appropriate user‐supplied assertions or reachability of invalid end states. The analyst can express security properties of specific attack actions that are not restricted to safety violations captured by a generic model checker. The described intruder model methodology was implemented within the SPIN model checker for verifying two security protocols, Micromint and PayWord. Copyright © 2009 John Wiley & Sons, Ltd.

This work introduces probabilistic model checking as a viable tool-assisted approach for systematically quantifying DoS security threats. The proposed analysis is based on a probabilistic attacker model implementing simultaneous N zombie participants, which subvert secure authentication features in communication protocols and electronic commerce systems. DoS threats are expressed as probabilistic reachability properties that are automatically verified through an appropriate Discrete Time Markov Chain representing the protocol participants and attacker models. The overall analysis takes place in a mature probabilistic model checking toolset called PRISM. We believe that the applied quantitative verification approach is a valuable means for comparing protocol implementations with alternative parameter choices, for optimal resistance to the analyzed threats.

Abstract Checkpointing has a crucial impact on systems' performance and fault‐tolerance effectiveness: excessive checkpointing results in performance degradation, while deficient checkpointing incurs expensive recovery. In distributed systems with independent checkpoint activities there is no easy way to determine checkpoint frequencies optimizing response‐time and fault‐tolerance costs at the same time. The purpose of this paper is to investigate the potentialities of a statistical decision‐making procedure. We adopt a simulation‐based approach for obtaining performance metrics that are afterwards used for determining a trade‐off between checkpoint interval reductions and efficiency in performance. Statistical methodology including experimental design, regression analysis and optimization provides us with the framework for comparing configurations, which use possibly different fault‐tolerance mechanisms (replication‐based or message‐logging‐based). Systematic research also allows us to take into account additional design factors, such as load balancing. The method is described in terms of a standardized object replication model (OMG FT‐CORBA), but it could also be applied in other (e.g. process‐based) computational models. Copyright © 2006 John Wiley & Sons, Ltd.

Recent developments in the field of object-based fault tolerance and the advent of the first OMG FT-CORBA compliant middleware raise new requirements for the design process of distributed fault-tolerant systems. In this work, we introduce a simulation-based design approach based on the optimum effectiveness of the compared fault tolerance schemes. Each scheme is defined as a set of fault tolerance properties for the objects that compose the system. Its optimum effectiveness is determined by the tightest effective checkpoint intervals, for the passively replicated objects. Our approach allows mixing miscellaneous fault tolerance policies, as opposed to the published analytic models, which are best suited in the evaluation of single-server process replication schemes. Special emphasis has been given to the accuracy of the generated estimates using an appropriate simulation output analysis procedure. We provide showcase results and compare two characteristic warm passive replication schemes: one with periodic and another one with load-dependent object state checkpoints. Finally, a trade-off analysis is applied, for determining appropriate checkpoint properties, in respect to a specified design goal.