nach oben

2019 | Buch

Kapitel lesen Erstes Kapitel lesen

Verification and Evaluation of Computer and Communication Systems

13th International Conference, VECoS 2019, Porto, Portugal, October 9, 2019, Proceedings

herausgegeben von: Pierre Ganty, Mohamed Kaâniche

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes the proceedings of the 13th International Conference on Veriﬁcation and Evaluation of Computer and Communication Systems ( VECoS 2019), held in Porto, Portugal, in October 2019.

The 7 full papers in this volume, presented together with two invited talks, were carefully reviewed and selected from 13 submissions.

The aim of the VECoS conference is to bring together researchers and practitioners in the areas of veriﬁcation, control, performance, and dependability evaluation in order to discuss state of the art and challenges in modern computer and communication systems in which functional and extra-functional properties are strongly interrelated. Thus, the main motivation for VECoS is to encourage the cross-fertilization between various formal veriﬁcation and evaluation approaches, methods and techniques, and especially those developed for concurrent and distributed hardware/software systems.

Inhaltsverzeichnis

Frontmatter

Modeling Concurrent Behaviors as Words

Abstract

Performing formal verification of concurrent systems involves partial order logics (here MSO with partial orders) for the specification of properties or of the concurrent system itself. A common structure for the verification of concurrent systems is so-called pomset. A pomset is a multiset of partially ordered events. The partial order relation describes causal dependencies of events. We propose a new word based model, namely Pre-Post-Pomset, making the exploration of pomsets space possible. In this paper, our new model stands to be a general model in the sense that some classical models used in the specification of concurrent systems (Synchronized product of systems, Mazurkiewicz traces or parallel series) can be specified within. Besides its general aspect, our model offers decidability results on the verification problem according to an MSO formula on pomsets.

Yohan Boichut, Jean-Michel Couvreur, Xavier Ferry, Mohamadou Tafsir Sakho

Non-Standard Zeno-Free Simulation Semantics for Hybrid Dynamical Systems

Abstract

Geometric-Zeno behavior is one of the most challenging problems in the analysis and simulation of hybrid systems. Geometric-Zeno solutions involve an accumulation of an infinite number of discrete events occurring in a finite amount of time. In models that exhibit geometric-Zeno, discrete events occur at an increasingly smaller distance in time, converging to a limit point according to a geometric series. In practice, simulating models of hybrid systems exhibiting geometric-Zeno is highly challenging, in that the simulation either halts or produces faulty results, as the time interval lengths are decreasing to arbitrary small positive numbers. Although many simulation tools for hybrid systems have been developed in the past years, none of them have a Zeno-free semantic model. All of them produce faulty results when simulating geometric-Zeno models. In this paper, we propose a non-standard Zeno-free mathematical formalism for detecting and eliminating geometric-Zeno during simulation. We derive sufficient conditions for the existence of geometric-Zeno behavior based on the existence of a non-standard contraction map in a complete metric space. We also provide methods for carrying solutions from pre-Zeno to post-Zeno. We illustrate the concepts with examples throughout the paper.

Ayman Aljarbouh

Static Detection of Event-Driven Races in HTML5-Based Mobile Apps

Abstract

HTML5-based mobile apps are developed using standard web technologies such as HTML5, CSS, JavaScript, so they may also face with event-based races as web apps. The races in such mobile apps can be caused by various sources of asynchronous events, especially, middlware framework events. For example, PhoneGap framework supports the lifecycle events for signaling states of an app like Android’s lifecycle and the resource access events for interacting with the platform resources such as contact, SMS, etc. When those events fire, it may generate nondeterministic execution orders of corresponding event handlers. Those nondeterminisms may raise data races among them.

In this paper, we introduce event-based races in HTML5-based mobile apps. Moreover, we propose a semi-automated approach combining static data flow analysis with manual code inspection for race detection. To evaluate it, we ran our proposed approach on a dataset of 1,926 HTML5-based mobile apps for detecting event-based races. Eventually, it scanned out totally 18 vulnerable apps. We manually inspected such vulnerable apps and discovered out 21 true races.

Phi Tuong Lau

Analysing Security Protocols Using Scenario Based Simulation

Abstract

In this paper, we present a methodology for analysing security protocols using scenario based simulation. A scenario of a potential attack specifies the flow but not the content of messages. Using scenarios can reduce the number of protocol runs to be explored during attack searching via simulation. The number of runs can be further reduced by minimizing the number of intruder’s generated messages. The intruder’s ability to generate messages is limited by considering: the expected message content and type matching. Our approach uses two tools that support the Abstract State Machines method: the AsmetaL for modelling purposes and the AsmetaS for performing the simulation. We propose a simple model for the specification of commutative encryption. Several protocols are examined to show the effectiveness of our method.

Farah Al-Shareefi, Alexei Lisitsa, Clare Dixon

Running on Fumes

Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis

Abstract

Gas is a measurement unit of the computational effort that it will take to execute every single operation that takes part in the Ethereum blockchain platform. Each instruction executed by the Ethereum Virtual Machine (EVM) has an associated gas consumption specified by Ethereum. If a transaction exceeds the amount of gas allotted by the user (known as gas limit), an out-of-gas exception is raised. There is a wide family of contract vulnerabilities due to out-of-gas behaviors. We report on the design and implementation of Gastap, a Gas-Aware Smart contracT Analysis Platform, which takes as input a smart contract (either in EVM, disassembled EVM, or in Solidity source code) and automatically infers gas upper bounds for all its public functions. Our bounds ensure that if the gas limit paid by the user is higher than our inferred gas bounds, the contract is free of out-of-gas vulnerabilities.

Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey

Estimating Latency for Synchronous Dataflow Graphs Using Periodic Schedules

Abstract

Synchronous Dataflow Graph (SDFG) is a formal tool widely used to model and analyze the behaviour of systems constrained by timing requirements. It has been successfully used in digital signal processing and manufacturing fields to specify and analyze the performance of embedded and distributed applications. Various performance indicators such as throughput, latency or memory consumption can be evaluated with SDFGs. This paper tackles the latency analysis for SDFG using periodic schedules.

Philippe Glanon, Selma Azaiez, Chokri Mraidha

Importance-Based Scheduling to Manage Multiple Core Defection in Real-Time Systems

Abstract

This paper presents an approach to support multiple permanent node failures in multicore real time systems. In the absence of failures, the system is scheduled with the PFair algorithm PD2. To overcome failures, a single spare core is provided and two protocols based on task importance are defined: The Recovery Time Distribution Protocol (RTDP) and the Graceful Degradation Protocol (GDP). When a single core fails, RTDP sets the system parameters such that all the tasks still meet their deadlines, although after a bounded delay. When several cores fail, GDP defines several modes corresponding to degraded execution. Different strategies are provided to decide which tasks are dropped in degraded modes. The experimentation of both protocols shows conclusive results. Tasks recover from the failure in a bounded delay with RTDP, whereas there are some missed deadlines with GDP. However, we exploit the experimental results to guide the designer on which elimination strategy to use.

Yves Mouafo Tchinda, Annie Choquet-Geniet, Gaëlle Largeteau-Skapin

Backmatter

Titel: Verification and Evaluation of Computer and Communication Systems
herausgegeben von: Pierre Ganty
Mohamed Kaâniche
Verlag: Springer International Publishing
Electronic ISBN: 978-3-030-35092-5
Print ISBN: 978-3-030-35091-8
DOI: https://doi.org/10.1007/978-3-030-35092-5

Springer Professional

Über dieses Buch

Inhaltsverzeichnis

Frontmatter

Modeling Concurrent Behaviors as Words

Non-Standard Zeno-Free Simulation Semantics for Hybrid Dynamical Systems

Static Detection of Event-Driven Races in HTML5-Based Mobile Apps

Analysing Security Protocols Using Scenario Based Simulation

Running on Fumes

Estimating Latency for Synchronous Dataflow Graphs Using Periodic Schedules

Importance-Based Scheduling to Manage Multiple Core Defection in Real-Time Systems

Backmatter

Premium Partner