A blockchain is a list of data blocks as a publicly distributed ledger, which are linked together using cryptography. By allowing Turing-complete programming languages to implement smart contracts, recent blockchains such as Ethereum can reduce needs in trusted intermediators, arbitrations and enforcement costs. However, subtle errors in smart contracts have induced an enormous financial loss—for examples, the DAO attack, Parity multisignature wallet attacks, and integer underflow/overflow attacks. To identify such errors in smart contracts, various researches are performed, which are based on static analysis and theorem proving. However, they only support inspection for pre-defined error patterns, or they cannot explore the whole searching space exhaustively or be fully automatic. Hence, in this paper, we propose a novel formal verification technique to analyze blockchain smart contracts by using ATL model checking. In our methodology, we represent the interaction between users and smart contracts into a two-player game and verify properties we want to check using MCMAS that is an efficient ATL model checker for multi-agent systems. Moreover, we present three case studies to show that our proposal can successfully identify subtle flaws in real world smart contracts.

Traditional planning assumes reachability goals and/or full observability. In this paper, we propose a novel solution for safety and reachability planning with partial observability. Given a planning domain, a safety property, and a reachability goal, we automatically learn a safe permissive plan to guide the planning domain so that the safety property is not violated and that can force the planning domain to eventually reach states that satisfy the reachability goal, regardless of how the planning domain behaves. Our technique is based on the active learning of regular languages and symbolic model checking. The planning method first learns a safe plan using the L ^* algorithm, which is an efficient active learning algorithm for regular languages. We then check whether the safe plan learned is also permissive by Alternating-time Temporal Logic (ATL) model checking. If the plan is permissive, it is indeed a safe permissive plan. Otherwise, we identify and add a safe string to converge a safe permissive plan. We describe an implementation of the proposed technique and demonstrate that our tool can efficiently construct safe permissive plans for four sets of examples.

Deep neural networks have achieved remarkable performance in various fields such as image recognition and natural language processing. However, recent research has revealed that even a small imperceptible perturbation can confound well-trained neural network models and yield incorrect answers. Such adversarial examples are regarded as a key hazard to the application of machine learning techniques to safety-critical systems, such as unmanned vehicle navigation and security systems. In this study, we propose an efficient technique for searching one-pixel attacks in deep neural networks, which are recently reported as an adversarial example. Using exhaustive search, our method can identify one-pixel attacks which existing methods cannot detect. Moreover, the method can adjust exhaustiveness to reduce the search space dramatically. However, it still identifies most attacks. We present our experiment using the MNIST data set to demonstrate that our adjustable search method efficiently identifies one-pixel attacks in well-trained deep neural networks, including convolutional layers.

Recent research has revealed that subtle imperceptible perturbations can deceive well-trained neural network models, leading to inaccurate outcomes. These instances, known as adversarial examples, pose significant threats to the secure application of machine learning techniques in safety-critical systems. In this paper, we delve into the study of one-pixel attacks in deep neural networks, recently reported as a kind of adversarial examples. To identify such one-pixel attacks, most existing methodologies rely on the differential evolution method, which utilizes random selection from the current population to escape local optima. However, the differential evolution technique might waste search time and overlook good solutions if the number of iterations is insufficient. Hence, in this paper, we propose a gradient ascent with momentum approach to efficiently discover good solutions for the one-pixel attack problem. As our method takes a more direct route to the goal compared to existing methods relying on blind random walks, it can effectively identify one-pixel attacks. Our experiments conducted on popular CNNs demonstrate that, in comparison with existing methodologies, our technique can detect one-pixel attacks significantly faster.

Recent studies have shown that deep neural networks can be misled by adversarial examples that involve only imperceptible perturbations. Among these, one-pixel attacks (OPA) represent an extreme yet powerful threat, as they alter only a single pixel of an input image while causing misclassification. While prior work has demonstrated the effectiveness of OPAs on low-resolution datasets, extending these attacks to high-resolution images poses a significant challenge due to the dramatic increase in the number of pixels and the resulting expansion of the search space. In this paper, we address this challenge by proposing a scalable one-pixel attack framework for deep neural networks on high-resolution images. The key difficulty in high-resolution OPAs lies in identifying a vulnerable pixel among tens of thousands of candidates under a black-box setting, where exhaustive pixel-wise probing is prohibitively expensive. To overcome this limitation, we decompose the attack into two phases. In the first phase, we efficiently identify a small set of promising pixel locations using a hierarchical patch-based search strategy, which iteratively prunes large image regions via coarse-grained patch perturbations, thereby substantially reducing the number of required model queries. In the second phase, for each selected pixel candidate, we search for adversarial RGB values using a black-box optimization method based on momentum-accelerated finite-difference gradient estimation. We evaluate our method on popular deep neural network architectures using high-resolution ImageNet images. The experimental results demonstrate that our approach achieves high attack success rates while significantly reducing query cost and improving the quality of the resulting adversarial perturbations compared to existing strategies.

Many programming languages provides mechanism to guarantee the error ranges of exact numbers and intervals. However, when they are integrated with unreliable approximated numbers, we cannot rely on the error-ranges anymore. Such unreliable error-ranges may cause serious errors in programs, and especially in safety critical systems they cost us huge amount of money and/or threaten human’s life. Hence, in this paper, we propose a novel number system to safely perform arithmetic operations with guaranteed error ranges. In the number system, exact numbers are separated from approximated numbers, and approximated numbers with strictly guaranteed error-ranges are again separated from unwarranted numbers such as floating-point numbers. A three-valued logic is also shipped with our number system to appropriately deal with uncertainties due to approximations. A prototype implementation of our number system in Python is demonstrated. With this module, we can more reliably execute operations on numbers and make judgments on the conditions involving numbers.