Reliability Analysis of the Proactive Transmission of Replicated Frames Mechanism over Time-Sensitive Networking

The Time-Sensitive Networking (TSN) Task Group has standardised different mechanisms to provide Ethernet with hard real-time guarantees and reliability in layer 2 of the network architecture. Specifically, TSN proposes using space redundancy to increase the reliability of Ethernet networks, but using space redundancy to tolerate temporary faults is not a cost-effective solution. For this reason, we propose to use time redundancy to tolerate temporary faults in the links of TSN-based networks. Specifically, in previous works we proposed the Proactive Transmission of Replicated Frames (PTRF) mechanism to tolerate temporary faults in the links. Now, in this work we present a series of models of TSN and PTRF developed using PRISM, a probabilistic model checker that can be used to evaluate the reliability of systems. After that, we carry out a parametric sensitivity analysis of the reliability achievable by TSN and PTRF and we show that we can increase the reliability of TSN-based networks using PTRF to tolerate temporary faults in the links of TSN networks. This is the first work that presents a quantitative analysis of the reliability of TSN networks.

Anonymously Establishing Digital Provenance in Reseller Chains

<p>An increasing number of products are exclusively digital items, such as media files, licenses, services, or subscriptions. In many cases customers do not purchase these items directly from the originator of the product but through a reseller instead. Examples of some well known resellers include GoDaddy, the iTunes music store, and Amazon. This thesis considers the concept of provenance of digital items in reseller chains. Provenance is defined as the origin and ownership history of an item. In the context of digital items, the origin of the item refers to the supplier that created it and the ownership history establishes a chain of ownership from the supplier to the customer. While customers and suppliers are concerned with the provenance of the digital items, resellers will not want the details of the transactions they have taken part in made public. Resellers will require the provenance information to be anonymous and unlinkable to prevent third parties building up large amounts of information on the transactions of resellers. This thesis develops security mechanisms that provide customers and suppliers with assurances about the provenance of a digital item, even when the reseller is untrusted, while providing anonymity and unlinkability for resellers . The main contribution of this thesis is the design, development, and analysis of the tagged transaction protocol. A formal description of the problem and the security properties for anonymously providing provenance for digital items in reseller chains are defined. A thorough security analysis using proofs by contradiction shows the protocol fulfils the security requirements. This security analysis is supported by modelling the protocol and security requirements using Communicating Sequential Processes (CSP) and the Failures Divergences Refinement (FDR) model checker. An extended version of the tagged transaction protocol is also presented that provides revocable anonymity for resellers that try to conduct a cloning attack on the protocol. As well as an analysis of the security of the tagged transaction protocol, a performance analysis is conducted providing complexity results as well as empirical results from an implementation of the protocol.</p>

Anonymously Establishing Digital Provenance in Reseller Chains

<p>An increasing number of products are exclusively digital items, such as media files, licenses, services, or subscriptions. In many cases customers do not purchase these items directly from the originator of the product but through a reseller instead. Examples of some well known resellers include GoDaddy, the iTunes music store, and Amazon. This thesis considers the concept of provenance of digital items in reseller chains. Provenance is defined as the origin and ownership history of an item. In the context of digital items, the origin of the item refers to the supplier that created it and the ownership history establishes a chain of ownership from the supplier to the customer. While customers and suppliers are concerned with the provenance of the digital items, resellers will not want the details of the transactions they have taken part in made public. Resellers will require the provenance information to be anonymous and unlinkable to prevent third parties building up large amounts of information on the transactions of resellers. This thesis develops security mechanisms that provide customers and suppliers with assurances about the provenance of a digital item, even when the reseller is untrusted, while providing anonymity and unlinkability for resellers . The main contribution of this thesis is the design, development, and analysis of the tagged transaction protocol. A formal description of the problem and the security properties for anonymously providing provenance for digital items in reseller chains are defined. A thorough security analysis using proofs by contradiction shows the protocol fulfils the security requirements. This security analysis is supported by modelling the protocol and security requirements using Communicating Sequential Processes (CSP) and the Failures Divergences Refinement (FDR) model checker. An extended version of the tagged transaction protocol is also presented that provides revocable anonymity for resellers that try to conduct a cloning attack on the protocol. As well as an analysis of the security of the tagged transaction protocol, a performance analysis is conducted providing complexity results as well as empirical results from an implementation of the protocol.</p>

TOrPEDO: witnessing model correctness with topological proofs

Model design is not a linear, one-shot process. It proceeds through refinements and revisions. To effectively support developers in generating model refinements and revisions, it is desirable to have some automated support to verify evolvable models. To address this problem, we recently proposed to adopt topological proofs, which are slices of the original model that witness property satisfaction. We implemented , a framework that provides automated support for using topological proofs during model design. Our results showed that topological proofs are significantly smaller than the original models, and that, in most of the cases, they allow the property to be re-verified by relying only on a simple syntactic check. However, our results also show that the procedure that computes topological proofs, which requires extracting unsatisfiable cores of LTL formulae, is computationally expensive. For this reason, currently handles models with a small dimension. With the intent of providing practical and efficient support for flexible model design and wider adoption of our framework, in this paper, we propose an enhanced—re-engineered—version of . The new version of relies on a novel procedure to extract topological proofs, which has so far represented the bottleneck of performances. We implemented our procedure within by considering Partial Kripke Structures (PKSs) and Linear-time Temporal Logic (LTL): two widely used formalisms to express models with uncertain parts and their properties. To extract topological proofs, the new version of converts the LTL formulae into an SMT instance and reuses an existing SMT solver (e.g., Microsoft ) to compute an unsatisfiable core. Then, the unsatisfiable core returned by the SMT solver is automatically processed to generate the topological proof. We evaluated by assessing (i) how does the size of the proofs generated by compares to the size of the models being analyzed; and (ii) how frequently the use of the topological proof returned by avoids re-executing the model checker. Our results show that provides proofs that are smaller ($$\approx $$ ≈ 60%) than their respective initial models effectively supporting designers in creating model revisions. In a significant number of cases ($$\approx $$ ≈ 79%), the topological proofs returned by enable assessing the property satisfaction without re-running the model checker. We evaluated our new version of by assessing (i) how it compares to the previous one; and (ii) how useful it is in supporting the evaluation of alternative design choices of (small) model instances in applied domains. The results show that the new version of is significantly more efficient than the previous one and can compute topological proofs for models with less than 40 states within two hours. The topological proofs and counterexamples provided by are useful to support the development of alternative design choices of (small) model instances in applied domains.

Modeling of a Generic Edge Computing Application Design

Edge computing applications leverage advances in edge computing along with the latest trends of convolutional neural networks in order to achieve ultra-low latency, high-speed processing, low-power consumptions scenarios, which are necessary for deploying real-time Internet of Things deployments efficiently. As the importance of such scenarios is growing by the day, we propose to undertake two different kind of models, such as an algebraic models, with a process algebra called ACP and a coding model with a modeling language called Promela. Both approaches have been used to build models considering an edge infrastructure with a cloud backup, which has been further extended with the addition of extra fog nodes, and after having applied the proper verification techniques, they have all been duly verified. Specifically, a generic edge computing design has been specified in an algebraic manner with ACP, being followed by its corresponding algebraic verification, whereas it has also been specified by means of Promela code, which has been verified by means of the model checker Spin.

Parametric Schedulability Analysis of a Launcher Flight Control System under Reactivity Constraints*

The next generation of space systems will have to achieve more and more complex missions. In order to master the development cost and duration of such systems, an alternative to a manual design is to automatically synthesize the main parameters of the system. In this paper, we present an approach for the specific case of the scheduling of the flight control of a space launcher. The approach requires two successive steps: (1) the formalization of the problem to be solved in a parametric formal model and (2) the synthesis of the model parameters with a tool. We first describe the problem of the scheduling of a launcher flight control, then we show how this problem can be formalized with parametric stopwatch automata; we then present the results computed by the parametric timed model checker IMITATOR. We enhance our model by taking into consideration the time for switching context, and we compare the results to those obtained by other tools classically used in scheduling.