Search

In traditional digital twin communication system testing, we can apply test cases as completely as possible in order to ensure the correctness of the system implementation, and even then, there is no guarantee that the digital twin communication system implementation is completely correct. Formal verification is currently recognized as a method to ensure the correctness of software system for communication in digital twins because it uses rigorous mathematical methods to verify the correctness of systems for communication in digital twins and can effectively help system designers determine whether the system is designed and implemented correctly. In this paper, we use the interactive theorem proving tool Isabelle/HOL to construct the formal model of the X86 architecture, and to model the related assembly instructions. The verification result shows that the system states obtained after the operations of relevant assembly instructions is consistent with the expected states, indicating that the system meets the design expectations.

Technological developments in semiconductors have created previously unheard-of chances for creativity, but they have also increased the danger of hardware Trojans, which are malevolent modifications introduced into integrated circuits (ICs) during the design or production phases. This research review addresses the changing landscape of threats and responses by examining the most recent advancements and trends in hardware trojan detection and prevention approaches. Proactive protections against Trojan insertion and dissemination include methods like cryptographic primitives, trust verification protocols, and hardware obfuscation. The field of detection approaches has expanded to include a multi-layered approach that integrates emerging technologies like artificial intelligence and machine learning with more established methods like testing and design-time analysis. Furthermore, it is possible to improve resistance to Trojan assaults while reducing performance overhead by incorporating hardware security features like physically unclonable functions and secure compartments directly into the IC architecture. Moreover, various prevention algorithms, detecting challenges and effects of the HT in recent applications are summarized with its solutions. [ABSTRACT FROM AUTHOR]

In embedded systems, the execution semantics of the real-time operating system (RTOS), which is responsible for scheduling and timely execution of concurrent processes, is crucial for the correctness of the overall system. However, existing approaches for the formal verification of embedded systems typically abstract from the RTOS completely, or provide a detailed and synthesizable formal model of the RTOS. While the former may lead to unsafe systems, the latter is not compatible with industrial design processes. In this paper, we present an approach for reusable abstract formal models that can be configured for custom RTOS. Our key idea is to formally capture common execution mechanisms of RTOS like preemptive scheduling, event synchronization, and communication abstractly in configurable timed automata models. These abstract formal models can be configured for a concrete custom RTOS, and they can be combined into a formal system model together with a concrete application. Our reusable models significantly reduce the manual effort of defining a formal model that captures concurrency and real-time behavior, together with the functionality of an application. The resulting formal model enables analysis, verification, and graphical simulation. We validate our approach by formalizing and analyzing a rescue robot application running the custom open source RTOS EV3RT. [ABSTRACT FROM AUTHOR]

The use of machine learning (ML) in airborne safety-critical systems requires new methods for certification, as the current standards and practices were defined and refined over decades with classical programming in mind and do not support this new development paradigm. This article provides an overview of the main challenges to the demonstration of compliance with regulation requirements raised by the use of ML and focuses on one particular case where the formal verification may become mandatory in future regulations, which is the verification of (partial) monotony properties. For this case, we propose a method to evaluate the monotony property using mixed integer linear programming. Contrary to the existing literature, our analysis provides a lower and upper bound of the space volume where the property does not hold, that we denote "Non-Monotonic Space Coverage". This work has several advantages: (i) our formulation of the monotony property works on discrete inputs, (ii) the iterative nature of our algorithm allows for refining the analysis as needed, and (iii) from an industrial point of view, the results of this evaluation are valuable for the aeronautical domain, where it can support the certification demonstration. We applied this method to an avionic case study (braking distance estimation using a neural network) where the verification of the monotony property is of paramount interest from a safety perspective. [ABSTRACT FROM AUTHOR]

We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language Dafny. In our methodology the ability to write specifications, implementations and to reason about correctness is a primary concern. We propose a simple, concise, yet powerful solution for reasoning about contracts that have external calls. This includes arbitrary re-entrancy, which is a major source of bugs and attacks in smart contracts. Although we do not yet have a compiler from Dafny to Ethereum Virtual Machine bytecode, the results we obtain from the Dafny code can reasonably be assumed to translate to contracts written in languages like Solidity. As a result our approach can readily be used to develop and deploy safer contracts. [ABSTRACT FROM AUTHOR]

Developing robotic applications with human–robot interaction for the service sector raises a plethora of challenges. In these settings, human behavior is essentially unconstrained as they can stray from the plan in numerous ways, constituting a critical source of uncertainty for the outcome of the robotic mission. Application designers require accessible and reliable frameworks to address this issue at an early development stage. We present a model-driven framework for developing interactive service robotic scenarios, allowing designers to model the interactive scenario, estimate its outcome, deploy the application, and smoothly reconfigure it. This article extends the framework compared to previous works by introducing an analysis of the impact of human errors on the mission's outcome. The core of the framework is a formal model of the agents at play—the humans and the robots—and the robotic mission under analysis, which is subject to statistical model checking to estimate the mission's outcome. The formal model incorporates a formalization of different human erroneous behaviors' phenotypes, whose likelihood can be tuned while configuring the scenario. Through scenarios inspired by the healthcare setting, the evaluation highlights how different configurations of erroneous behavior impact the verification results and guide the designer toward the mission design that best suits their needs. [ABSTRACT FROM AUTHOR]

In this paper, we prove the measurability of an event for which a general continuous–time stochastic process satisfies the continuous–time Metric Temporal Logic (MTL) formula. Continuous–time MTL can define temporal constraints for physical systems naturally. Several previous studies deal with the probability of continuous MTL semantics for stochastic processes. However, proving measurability for such events is not an obvious task, even though it is essential. The difficulty comes from the semantics of “until operator,” which is defined by the logical sum of uncountably many propositions. Given the difficulty in proving such an event’s measurability using classical measure-theoretic methods, we employ a theorem from stochastic analysis. This theorem is utilized to prove the measurability of hitting times for stochastic processes, and it stands as a profound result within the theory of capacity. Next, we provide an example that illustrates the failure of probability approximation when discretizing the continuous semantics of MTL–formulas with respect to time. Additionally, we prove that the probability of the discretized semantics converges to that of the continuous semantics when we impose restrictions on diamond operators to prevent nesting. [ABSTRACT FROM AUTHOR]

Cloud autoscaling is an important mechanism to dynamically manage cloud system resources with uncertain workload demands. The common goal in developing such a mechanism is to produce correct-by-design scaling policies that contribute to a reliable autoscaling component. A promising approach is formal verification, specifically probabilistic model checking (PMC), used to model and assess cloud scaling processes and policies. Utilizing the appropriate formal models effectively for carrying out verification tasks is one of the important factors in gaining significant insights. This is a great challenge dealt by the responsible party (e.g., cloud architects, engineers) in maximizing the benefits of PMC for their further decision-making (e.g., deploying the verified policies). In response to this challenge, we propose an approach to formalize and assess the cloud scaling process based on two formal models, namely, Markov Decision Process (MDP) and discrete-time Markov Chain (DTMC), and using PMC. We treat these two models independently for modeling similar cloud scaling contexts and assess the relevant aspects for gaining significant insights. Our approach consists of three main phases: modeling, encoding, and assessment. In our assessment, which includes complexity, performance, and sensitivity analyses, we have identified distinct sensitivities in the DTMC and MDP models. Specifically, DTMC is more sensitive to over-provisioning events, while MDP is more sensitive to under-provisioning events. These sensitivities are mainly influenced by two critical parameters: the initial number of VMs and the minimum number of VMs. Across various sample sizes, DTMC showed an increase in average latency violations from 53 to 209 for over-provisioning events, while MDP demonstrated a decrease in average latency violations from 88 to 23 for under-provisioning events. [ABSTRACT FROM AUTHOR]

Power side-channel attacks allow an adversary to efficiently and effectively steal secret information (e.g., keys) by exploiting the correlation between secret data and runtime power consumption, hence posing a serious threat to software security, particularly cryptographic implementations. Masking is a commonly used countermeasure against such attacks, which breaks the statistical dependence between secret data and side-channel leaks via randomization. In a nutshell, a variable is represented by a vector of shares armed with random variables, called masking encoding, on which cryptographic computations are performed. While compositional verification for the security of masked cryptographic implementations has received much attention because of its high efficiency, existing compositional approaches either use implicitly fixed pre-conditions that may not be fulfilled by state-of-the-art efficient implementations, or require user-provided hard-coded pre-conditions that are time consuming and highly non-trivial, even for an expert. In this article, we tackle the compositional verification problem of first-order masking countermeasures, where first-order means that the adversary is allowed to access only one intermediate computation result. Following the literature, we consider countermeasures given as gadgets, which are special procedures whose inputs are masking encodings of variables. We introduce a new security notion parameterized by an explicit pre-condition for each gadget, as well as composition rules for reasoning about masking countermeasures against power side-channel attacks. We propose accompanying efficient algorithms to automatically infer proper pre-conditions, based on which our new compositional approach can efficiently and automatically prove security for masked implementations. We implement our approaches as a tool MaskCV and conduct experiments on publicly available masked cryptographic implementations including 10 different full AES implementations. The experimental results confirm the effectiveness and efficiency of our approach. [ABSTRACT FROM AUTHOR]

The IOTA Extended UTXO (IOTA EUTXO) model extends the UTXO blockchain to include features like smart contracts and non-fungible tokens. In this work, we show that the IOTA EUTXO model maintains the base correctness properties of the UTXO model while extending it with extra functionality. We achieve this by specifying and verifying the essential concepts of the base UTXO model and the extensions proposed by IOTA using the Isabelle proof assistant. The specification is designed to be modular and extensible, meaning it can be used as a foundation for further research of the UTXO and IOTA EUTXO models. [ABSTRACT FROM AUTHOR]

A cryptocurrency is a digital currency that enables online transactions for various products and services. Cryptocurrencies are deployed over public blockchains which have the transactions duplicated and dispersed across multiple nodes within a computer network. This decentralized mechanism is devised in order to achieve reliability in a network consisting of unreliable nodes. Privacy, anonymity and security have become crucial in this context. For that reason, formal and mathematical approaches are gaining popularity in order to guarantee the correctness of the cryptocurrency implementations. Mimblewimble is a privacy-oriented cryptocurrency technology which provides security and scalability properties that distinguish it from other protocols of its kind. Mimblewimble combines confidential transactions, CoinJoin and cut-through to achieve a higher level of privacy and security, as well as, scalability. In this work, we present and discuss these security properties and outline the basis of a model-driven verification approach to address the certification of the correctness of the protocol implementations. In particular, we propose an idealized model that is key in the described verification process. Then, we identify and precisely state the conditions for our model to ensure the verification of relevant security properties of Mimblewimble. In addition, we analyze the Grin and Beam implementations of Mimblewimble in their current state of development. We present detailed connections between our model and their implementations regarding the Mimblewimble structure and its security properties. Finally, we analyze the Litecoin soft-fork that enhances privacy over the blockchain based on Mimblewimble features.

The subject: This study focuses on improving the quality of Cyber-Physical System (CPS) software by eliminating incorrect usage of units of measurement and orientation in C/C++ programs. Incorrect usage often leads to critical errors that conventional systems cannot effectively prevent. Manual examination of code using dimensional and orientation analysis can detect these errors in physical equations, but these methods become impractical when dealing with complex physical computations. Objectives: As suggested by Siano, the proposed approach uses physical quantities and prefixes defined by the International System of Units and orientation operations on physical objects. The elaborated system incorporates dimensional and orientation analysis and metaprogramming techniques. The methods used are dimensional & orientational analysis and metaprogramming. The following results were obtained: ensuring consistency of the units, incorporating orientation operations into the programming model for accurately handling physical object rotations and alignments, and using Siano’s work to precisely manipulate object orientation, thereby reducing the likelihood of orientation-related errors. Checking physical dimensions and orientations during the compilation stage identifies potential software defects before code execution, thereby reducing debugging time and lowering the cost of addressing issues later in development. The elaborated system represents a crucial step towards safer and more dependable Cyber-Physical System applications. This approach allows us to identify approximately 90% of incorrect usage of program variables; additionally, it detects over 50% of erroneous operations during compilation and execution of large-scale programs in real-world conditions. Conclusions. Scientific novelty: it proposed and developed a specialized C++-type library for formal compile-time software verification of Cyber-Physical Systems software. The proposed C++-type library leverages dimensional and orientational analysis to enhance software quality, reliability, and real-time formal verification. Although the proposed method for formal verification is not tailor-made for cyber-physical objects and systems, given its primary focus on software-level concerns, it does exhibit adaptability for verifying general-purpose software that incorporates various physical parameters. This versatility extends to diverse domains such as educational, gaming, and simulation software.

Modeling and verification are crucial in designing traffic light control systems, guaranteeing these systems meet desired operational properties and handle dynamic traffic conditions effectively. The design process involves addressing complexities such as route intricacy, congestion, timing, and prioritization, especially important in areas with multiple interconnected intersections. A key aspect of this process is developing a scalable model, essential for adapting to various traffic scenarios and intersection configurations. This paper presents a method using UPPAAL, a timed-automata tool, for modeling and verifying smart traffic light systems. We focus on creating scalable models, facilitating effective synchronization across intersections. Our approach includes templates and frameworks to assist in formalizing traffic light designs, emphasizing verification of safety, structural integrity, and performance. The results of our study reveal a significant usability in verification approaches through the use of formal model templates. Additionally, the model’s phases and stages, complete with adaptable time schedules, show flexibility in environments with variable parameters.

Bounded Model Checking (BMC) is one of the most prominent approaches used as a falsification engine, capable of identifying counterexamples of bounded length, in a scalable and sustainable way. Nevertheless, in the context of a portfolio-based verification suite, BMC can benefit from potential interaction with other engines, exploiting their capabilities and partial results as a form of application-dependant learning. In the past, previous works tackled the issue of using over-approximated state sets generated via Binary Decision Diagrams (BDD) based traversals. In a sense, BDD engines can be considered as external tools, whereas interpolants are directly related to BMC problems. Since interpolants come from Boolean satisfiability (SAT) refutation proofs, their role as a SAT-based learning can be potentially higher. Furthermore, their integration is more tightly linked to the BMC problem at hand. In this paper we aim at improving the efficiency of SAT calls in BMC problems, exploiting interpolation-based invariants computed over different cut points, as additional constraints for BMC problems. We experimentally evaluate costs and benefits of our proposed approach on a set of publicly available model checking problems.

The precise generation of train control curves for the on-board Automatic Train Protection (ATP) of the Chinese Train Control System Level 2 (CTCS-2) relies significantly on accurate train control engineering data, which serves as a critical element in ensuring the safe operation of trains. However, the traditional verification methods of train control engineering data depend on manual validation, which lacks timeliness and completeness and makes it easy to overlook potential errors. On the other hand, traditional verification rules are derived from railway technical specifications and standards, expressed in textual language that is often ambiguous, which leads to insufficient completeness in data verification. To address these challenges, this paper proposes a formal verification method for train control engineering data based on a Reduced Ordered Binary Decision Diagram (ROBDD). First, the attribute constraints of the train control data and the implicit constraint relations between different data objects are mined using existing railway technical specifications and expert knowledge of railway signals. These constraints are then converted into Boolean function models. Second, we formulate the ROBDD generation algorithm and the evaluation decision algorithm of the Boolean function using the equivalent canonical data structure ROBDD of the Boolean function. Finally, based on the train control engineering data from actual passenger-dedicated lines, the automatic verification method is developed by constructing four types of “mutation” data, including mutate, swap, add, and remove. The test cases indicate that our proposed formal verification method is feasible and capable of achieving high efficiency and completeness in the verification of CTCS-2 level train control engineering data.

Trust certification through so-called trust seals is a common strategy to help users ascertain the trustworthiness of a system. In this study, we examined trust seals for AI systems from two perspectives: (1) In a pre-registered online study participants, we asked whether trust seals can increase user trust in AI systems, and (2) qualitatively, we investigated what participants expect from such AI seals of trust. Our results indicate mixed support for the use of AI seals. While trust seals generally did not affect the participants’ trust, their trust in the AI system increased if they trusted the seal-issuing institution. Moreover, although participants understood verification seals the least, they desired verifications of the AI system the most.

This article proposes a method for the automatic generation of a plant model and monitoring using process mining algorithms based on recorded event logs. The behavioral traces of the system are captured by recording event logs during plant operation in either manual control mode or with an automatic controller. Process discovery algorithms are then applied to extract the logic of the process behavior properties from the recorded event logs. The result is represented as a Petri net, which is used to construct the state machine of the plant model and monitor and is in accordance with the IEC 61499 Standard. The monitor is implemented as a function block and can be deployed in real time to trigger an error signal whenever there is a deviation from the actual process scenario. The plant model and controller are connected in a closed loop and are used for the formal verification of the system with the help of the “fb2smv” converter and symbolic model checking tool NuSMV.

In concurrent transactional systems, a phantom read occurs when a transaction retrieves a set of data, and simultaneously, new data is inserted, updated, or removed from that set by one or more other transactions, leading to unexpected data being read. In Hyperledger Fabric (HF), a popular enterprise-grade framework for developing permissioned blockchain platforms, phantom reads are detected during the transaction validation phase. It inspects the values from read operations and checks their consistency, also re-executing some domain-specific read operations called range queries. However, being HF based on an optimistic concurrency control model, managing an excessive number of conflicts related to phantom reads could result in sudden system slowdowns. Additionally, some kind of range queries are not considered in the validation and verification process. For the latter, the re-execution is not performed and checks are not provided leading to undetected phantom reads when the values returned from them are written to the ledger. Hence, the burden of implementing phantom read-free applications (i.e., smart contracts) is on the developers, who need to correctly manage the read instructions in the code and use automatic verification tools to detect any unsafe implementations leading to system slowdowns and undetectable phantom reads. In this paper, we explore the phantom reads detection problem at the smart contract level and demonstrate how a verification approach through formal methods can identify possible bottlenecks caused by phantom reads and mitigate range query risks, outperforming the current state-of-the-art and state-of-the-practice for their detection. Our approach is implemented with GoLiSA, a semantic static analyzer based on abstract interpretation for Go applications.

Universal Subscriber Identity Module (USIM) is an essential part of the mobile network mainly for providing identification and authentication of the subscriber. The activation and deactivation of USIMs are the two most critical services that must be supported by Mobile Network Operators (MNOs). The current solutions suffer from several limitations such as the lack of round-the-clock services and the presence of a single point of failure. In this paper, we propose a blockchain-based scheme for USIM management. Each MNO creates its own smart contract and publishes its address to subscribers. Subscribers can then directly submit their requests by registering a transaction that invokes a specific function of the smart contract. The proposed scheme provides an anytime-anywhere service while at the same time it leverages the benefits of blockchain technology, such as a decentralized architecture that prevents Denial-of-Service (DoS) attacks, as well as a secure auditable log and payment using cryptocurrency. Moreover, we provide a security proof for the scheme through formal verification. Our results demonstrate that our scheme ensures subscriber privacy while providing mutual authentication among participants. Finally, our evaluation on the Ethereum blockchain confirms the efficiency of the scheme in terms of both transaction and execution costs.