Search

Safety-critical embedded systems must maintain their functionality even in the presence of single permanent hardware failure. Naive redundancy of hardware is often unaffordable and impractical, therefore alternative strategies must be explored for minimal cost fault tolerance. The objective of this article is to propose a methodology to evaluate formally safety strategies using satisfiability modulo theory solvers. Practically, the approach consists in providing a bounded model checking demonstration applied to the formal model of hardware. We show the capabilities of the approach on an efficient hardware accelerator designed to perform parallel computations of matrix multiplications and convolutions. [ABSTRACT FROM AUTHOR]

Traditional IoT authentication methods, often centralized and reliant on a Trusted Third Party (TTP), face issues like high communication costs and vulnerability to data loss. Blockchain-based Internet of Things (IoT) authentication can effectively solve the problems brought by traditional IoT authentication. Because the authentication schemes are usually deployed on a large number of IoT devices it would be extremely expensive when there are issues to be fixed after the authentication schemes is deployed. Performing verification early at design time can alleviate this problem. To focus on these requirements, this article proposes a formal verification framework for blockchain-based IoT authentication (FVF-BIoT). Specifically, we design data type mapping and the conversion of elements in smart contracts for the authentication. Then we formalize the smart contracts into formal models in the interactive theorem prover Coq. Several algorithms are presented for the conversion of the smart contracts and the generation of examples. Examples and security properties related to contracts are described in the form of theorems, which are also proved by Coq. Through a case study, we not only demonstrate the effectiveness of the FVF-BIoT framework in ensuring the security and reliability of blockchain technology for IoT authentication but also highlight its innovative integration of formal verification processes. This distinctly addresses the previously unmet need for rigorous, mathematically proven security validations in the design and deployment of blockchain-based IoT authentication methods. [ABSTRACT FROM AUTHOR]

The rapid evolution of mobile and optical communication technologies is driving the transition from 5G to 6G networks. This transition inevitably brings about changes in authentication scenarios, as new security demands emerge that go beyond the capabilities of existing frameworks. Therefore, it is necessary to address these evolving requirements and the associated key challenges: ensuring Perfect Forward Secrecy (PFS) to protect communications even if long-term keys are compromised and integrating Post-Quantum Cryptography (PQC) techniques to defend against the threats posed by quantum computing. These are essential for both radio and optical communications, which are foundational elements of future 6G infrastructures. The DMRN Protocol, introduced in 2022, represents a major advancement by offering both PFS and PQC while maintaining compatibility with existing 3rd Generation Partnership Project (3GPP) standards. Given the looming quantum-era challenges, it is imperative to analyze the protocol's security architecture through formal verification. Accordingly, we formally analyze the DMRN Protocol using SVO logic and ProVerif to assess its effectiveness in mitigating attack vectors, such as malicious or compromised serving networks (SNs) and home network (HN) masquerading. Our research found that the DMRN Protocol has vulnerabilities in key areas such as mutual authentication and key exchange. In light of these findings, our study provides critical insights into the design of secure and quantum-safe authentication protocols for the transition to 6G networks. Furthermore, by identifying the vulnerabilities in and discussing countermeasures to address the DMRN Protocol, this study lays the groundwork for the future standardization of secure 6G Authentication and Key Agreement protocols. [ABSTRACT FROM AUTHOR]

Electronic examination serves as an efficient method for assessing learning outcomes, yet the integration of computers into exam processes introduces potential for unreliability. In this article, we propose a formal model for electronic examinations using timed automata, providing a structured approach to understanding and managing the complexities. The electronic examination process is modeled by defining four UPPAAL templates, i.e., candidate, administrator, invigilator, and examiner. Crucial properties specific to electronic examination are encoded as specifications in UPPAAL. Verification against these properties demonstrates the validity and reliability of this model. The modelable and verifiable electronic examination designed with UPPAAL suggests great potential for deeper exploration in trustworthy digital education. [ABSTRACT FROM AUTHOR]

This paper introduces an innovative translation validation framework designed for MLIR-based compilers, which has garnered considerable prominence in fields such as machine learning, high-performance computing and hardware design. Despite rigorous testing, compilers based on MLIR might still induce incorrect results and undefined behaviors, necessitating verification work. Our framework first takes a pair of MLIR programs as inputs and check their function signature's compatibility before encoding them into SMT expressions. Then it uses the Z3 SMT solver to check whether the target program refines the source program. Our framework transcends the dialect limitations of past solutions, thereby providing validation support to a wider range of MLIR-based compilers. We demonstrate its effectiveness through evaluations on prominent open-source MLIR-based compilers, where we identified bugs and undefined behaviors. We further demonstrate the capability of this framework by validating two practical deep-learning accelerator designs. [ABSTRACT FROM AUTHOR]

Verification of asynchronous distributed programs is challenging due to the need to reason about numerous control paths resulting from the myriad interleaving of messages and failures. In this paper, we propose an automated bookkeeping method based on message chains. Message chains reveal structure in asynchronous distributed system executions and can help programmers verify their systems at the message passing level of abstraction. To evaluate our contributions empirically we build a verification prototype for the P programming language that integrates message chains. We use it to verify 16 benchmarks from related work, one new benchmark that exemplifies the kinds of systems our method focuses on, and two industrial benchmarks. We find that message chains are able to simplify existing proofs and our prototype performs comparably to existing work in terms of runtime. We extend our work with support for specification mining and find that message chains provide enough structure to allow existing learning and program synthesis tools to automatically infer meaningful specifications using only execution examples.

Satellite internet of things (satellite IoT) has been utilized to achieve the integration of space-ground, human-thing connection, and information interaction through the satellite communication network and various types of spaceborne and ground terminal devices. It possesses advantages that are boundless in air and unobstructed on ground, as well as characteristics such as large-scale coverage, highly open links, dynamically changing topologies, limited terminal resources, and long communication latency. In order to achieve the safe and efficient utilization of satellite IoT resources, a trust evaluation-based terminal authentication method for satellite IoT was proposed, which could optimize the authentication strategy by evaluating the trust of terminal devices. A trust evaluation mechanism for satellite IoT terminals was proposed for two scenarios: terminals that had recently undergone strong authentication and had been granted credit by strongly authenticated nodes. A dynamically adjusted trust measurement and evaluation model was characterized based on direct trust and indirect trust. Secondly, a trust evaluation-based access authentication protocol for satellite IoT was designed, which adopted a matching authentication mechanism according to the trust degree of the device. This allowed for the simplification of the subsequent authentication process for high-trust devices and provided differential authentication services for different terminal devices under the same authentication strategy framework. The security of the protocol was comprehensively analyzed using non-formal methods and Tamarin formal tools, and the effectiveness of the protocol was verified by experiments. The protocol was shown to be capable of reducing the overall authentication overhead and simplifying the authentication process with trust.

With the growing advances in Internet of Things (IoT) technology, it has become an indispensable part of many areas like home automation, industries, medical equipment, etc. Thus, the security of the IoT hardware and software is of utmost importance. The availability of secure IoT software components allows for better confidence in the use of IoT devices for consumers. IoT operating systems are core software components of the IoT ecosystem. There are a lot of IoT operating systems (OSes) available, but Real-time Operating System for IoT (RIOT) is one of the most commonly used open-source OS used by universities and businesses. As the RIOT source code is written in C, it inherently has some security vulnerabilities. With IoT devices having the characteristic of limited battery and computational capability, it is very challenging to detect cyber-attacks online. This would necessitate more rigorous security checks being performed on the device prior to deployment. For the security of the RIOT OS, the analysis techniques used in highly critical domains can also be applied to IoT software. Thus, the purpose of this work is to apply techniques such as formal verification to the crypto module of RIOT using a software analysis platform for C code, namely Frama-C in order to analyze the security aspects of the module. [ABSTRACT FROM AUTHOR]

Formally verified compilers and formally verified static analyzers are a solution to the problem that certain industries face when they have to demonstrate to authorities that the object code they run truly corresponds to its source code and that it satisfies certain properties. From a scientific and technological point of view, they are a challenge: not only a number of nontrivial invariants and algorithms must be proved to be correct, but also the implementation must be reasonably effective so that the tools operate within reasonable time. Many optimizations in compilers rely on static analysis, and thus a formally verified compiler entails formally verified static analyses. In this paper, we explain some difficulties, possible solutions, design choices, and trade-offs pertaining to verified static analysis, in particular, when the solution of the analysis is expressed as some form of tree, map, or set. [ABSTRACT FROM AUTHOR]

Copyright of Chinese Journal of Network & Information Security is the property of Beijing Xintong Media Co., Ltd. and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)

Current practice in simulation and implementation of robot controllers is usually undertaken with guidance from high-level design diagrams and pseudocode. Thus, no rigorous connection between the design and the development of a robot controller is established. This paper presents a framework for designing robotic controllers with support for automatic generation of executable code and automatic property checking. A state-machine based notation, RoboChart, and a tool (RoboTool) that implements the automatic generation of code and mathematical models from the designed controllers are presented. We demonstrate the application of RoboChart and its related tool through a case study of a robot performing an exploration task. The automatically generated code is platform independent and is used in both simulation and two different physical robotic platforms. Properties are formally checked against the mathematical models generated by RoboTool, and further validated in the actual simulations and physical experiments. The tool not only provides engineers with a way of designing robotic controllers formally but also paves the way for correct implementation of robotic systems. [ABSTRACT FROM AUTHOR]

Controlling access to critical zones by drones is crucial for ensuring safety and efficient operations in various applications. In this research, we propose a strategy for controlling the access of a set of drones to a critical zone using timed automata and UPPAAL. UPPAAL is a model checker and simulator for real-time systems, which allows for the modeling, simulation, and verification of timed automata. Our system consists of six drones, a controller, and a buffer, all modeled as timed automata. We present a formal model capturing the behavior and interactions of these components, considering the constraints of allowing only one drone in the critical zone at a time. Timed automata are a powerful formalism for modeling and analyzing real-time systems, as they can capture the temporal aspects of system behavior. The advantages of using timed automata include the ability to model time-critical systems, analyze safety and liveness properties, and verify the correctness of the system. We design a strategy that involves signaling the approaching drones, preventing collisions, and ensuring orderly access to the critical zone. We utilize UPPAAL for simulating and verifying the system, including the evaluation of properties such as validation properties, safety properties, liveness properties, and absence of deadlocks. However, a limitation of timed automata is that they can become complex and difficult to model for large-scale systems, and the analysis can be computationally expensive as the number of components and behaviors increases. Through simulations and formal verification, we demonstrate the effectiveness and correctness of our proposed strategy. The results highlight the ability of timed automata and UPPAAL to provide reliable and rigorous analysis of drone access control systems. Our research contributes to the development of robust and safe strategies for managing drone operations in critical zones. [ABSTRACT FROM AUTHOR]

Certificateless Proxy Signature (CLPS) offers a comprehensive authentication mechanism to ensure the optimal solutions from modern forgery attacks in Industrial Internet of Things (IIoTs) environment. CLPS is part of certificateless public key cryptography (CL-PKC) and has the benefits of eradicating many issues like key distribution problem. Although costly computational processing capabilities are consumed by smart devices during authentication process. This article proposed an authentication scheme for CLPS by using the mathematical cryptographic curve concepts of Hyper Elliptic Curve (HEC) to provide a secure and optimized communication approach in IIoTs environment. The arises key distribution problem in CLPS is also fixed. The scrutinized security analysis of proxy signature and delegation signature were performed to tackle different attacks like Machine-in-the-middle Attack (MiTM), Replay Attack, Key Replacement Attack, Impersonation Attack, and Chosen Message Attack. Due to HEC-DLP the forgery attack cannot succeeded. Finally, the proposed work is formally verified through the AVISPA tool. The comprehensive performance evaluation shows that the total computational cost is reduced to 49.48% and the communication overhead size is reduced to 49.57% with a comparative analysis of existing schemes. Thus, the proposed approach eradicates key distribution problems with an equal security level of RSA and ECC. [ABSTRACT FROM AUTHOR]

Neural networks as a machine learning technique are increasingly deployed in various domains. Despite their performance and their continuous improvement, the deployment of neural networks in safety-critical systems, in particular for autonomous mobility, remains restricted. This is mainly due to the lack of (formal) specifications and verification methods and tools that allow for having sufficient confidence in the behavior of the neural-network-based functions. Recent years have seen neural network verification getting more attention; many verification methods were proposed, yet the practical applicability of these methods to real-world neural network models remains limited. The main challenge of neural network verification methods is related to the computational complexity and the large size of neural networks pertaining to complex functions. As a consequence, applying abstraction methods for neural network verification purposes is seen as a promising mean to cope with such issues. The aim of abstraction is to build an abstract model by omitting some irrelevant details or some details that are not highly impacting w.r.t some considered features. Thus, the verification process is made faster and easier while preserving, to some extent, the relevant behavior regarding the properties to be examined on the original model. In this article, we review both the abstraction techniques for activation functions and model size reduction approaches, with a particular focus on the latter. The review primarily discusses the application of abstraction techniques on feed-forward neural networks and explores the potential for applying abstraction to other types of neural networks. Throughout the article, we present the main idea of each approach and then discuss its respective advantages and limitations in detail. Finally, we provide some insights and guidelines to improve the discussed methods. [ABSTRACT FROM AUTHOR]

In recent years, formal verification has emerged as a crucial method for assessing security against Side-Channel attacks of masked implementations, owing to its remarkable versatility and high degree of automation. However, formal verification still faces technical bottlenecks in balancing accuracy and efficiency, thereby limiting its scalability. Former tools like maskVerif and CocoAlma are very efficient but they face accuracy issues when verifying schemes that utilize properties of Boolean functions. Later, SILVER addressed the accuracy issue, albeit at the cost of significantly reduced speed and scalability compared to maskVerif. Consequently, there is a pressing need to develop formal verification tools that are both efficient and accurate for designing secure schemes and evaluating implementations. This paper’s primary contribution lies in proposing several approaches to develop a more efficient and scalable formal verification tool called Prover, which is built upon SILVER. Firstly, inspired by the auxiliary data structures proposed by Eldib et al. and optimistic sampling rule of maskVerif, we introduce two reduction rules aimed at diminishing the size of observable sets and secret sets in statistical independence checks. These rules substantially decrease, or even eliminate, the need for repeated computation of probability distributions using Reduced Ordered Binary Decision Diagrams (ROBDDs), a time-intensive procedure in verification. Subsequently, we integrate one of these reduction rules into the uniformity check to mitigate its complexity. Secondly, we identify that variable ordering significantly impacts efficiency and optimize it for constructing ROBDDs, resulting in much smaller representations of investigated functions. Lastly, we present the algorithm of Prover, which efficiently verifies the security and uniformity of masked implementations in probing model with or without the presence of glitches. Experimental results demonstrate that our proposed tool Prover offers a better balance between efficiency and accuracy compared to other state-of-the-art tools (IronMask, CocoAlma, maskVerif, and SILVER). In our experiments, we also found an S-box that can only be verified by Prover, as IronMask cannot verify S-boxes, and both CocoAlma and maskVerif suffer from false positive issues. Additionally, SILVER runs out of time during verification.

Smart contracts, being security-critical code, facilitate consensus among players and ensure secure and accurate value transfer, and formal verification is necessary to guarantee functional correctness of contracts. Game theory serves as one of the tools in formal verification by assessing whether the outcomes of contract executions meet the expected goals. While most studies employing game theory to verify smart contract functionality assume rational players, in practice, players may invoke and deploy smart contracts involving irrational behavior, casting doubt on the correctness of verification results. The aim of this study is to propose an alternative game model to verify smart contract functionality in dynamic player interactions where irrational behavior is involved. Specifically, a belief-based smart contract execution game (BSC-game) model was introduced, utilizing belief – the probability that a player believes in the irrationality of others – to capture how the irrational behavior of others affects a player’s contract execution decisions. Reasonable economic incentives were introduced to encourage honest behavior of players. Moreover, a computationally feasible method was designed to update players’ beliefs in large-scale dynamic smart contract executions. Theoretical analysis discloses the existence of equilibrium in the BSC-game, as well as the conditions for the number of faulty players within the system’s fault tolerance. We conducted the simulation experiments, and verified the business-oriented smart contract written in G language by the BSC-game model. The results further indicate that although players’ beliefs impact their decisions to execute contracts, reasonable economic incentives can motivate players to execute contracts honestly. This ensures that smart contract functionality aligns with expected goals, showing that the BSC-game model can verify and guarantee the correctness of contract functions. This new approach significantly contributes to bolstering smart contract security and credibility, positively influencing blockchain stability.

Electronic examination serves as an efficient method for assessing learning outcomes, yet the integration of computers into exam processes introduces potential for unreliability. In this article, we propose a formal model for electronic examinations using timed automata, providing a structured approach to understanding and managing the complexities. The electronic examination process is modeled by defining four UPPAAL templates, i.e., candidate, administrator, invigilator, and examiner. Crucial properties specific to electronic examination are encoded as specifications in UPPAAL. Verification against these properties demonstrates the validity and reliability of this model. The modelable and verifiable electronic examination designed with UPPAAL suggests great potential for deeper exploration in trustworthy digital education.