This paper presents a formal approach to verify arithmetic circuits using symbolic computer algebra. Our method describes arithmetic circuits directly with high-level mathematical objects based on weighted number systems and arithmetic formulae. Such circuit description can be effectively verified by polynomial reduction techniques using Grobner Bases. In this paper, we describe how the symbolic computer algebra can be used to describe and verify arithmetic circuits. The advantageous effects of the proposed approach are demonstrated through experimental verification of some arithmetic circuits such as multiply-accumulator and FIR filter. The result shows that the proposed approach has a definite possibility of verifying practical arithmetic circuits.

This paper presents an enhanced side-channel attack using a phase-based waveform matching technique. Conventionally, side-channel attacks such as Simple Power Analysis (SPA) and Differential Power Analysis (DPA) capture signal waveforms (e.g., power traces) with a trigger signal or a system clock, and use a statistical analysis of the waveforms to reduce noise and to retrieve secret information. However, the waveform data often includes displacement errors, and this degrades the accuracy of the statistical analysis. The use of a Phase-Only Correlation (POC) technique makes it possible to estimate the displacements between the signal waveforms with higher resolution than the sampling resolution. The accuracy of side-channel attacks can be enhanced using the POC-based matching method. Also, a popular DPA countermeasure of creating distorted waveforms with random delays can be defeated by our method. In this paper, we demonstrate the advantages of the proposed method in comparison with conventional approaches of experimental DPA and Differential ElectroMagnetic Analysis (DEMA) against DES software and hardware implementations.

This paper presents a graph-based approach to designing arithmetic circuits over Galois fields (GFs) using normal basis representations. The proposed method is based on a graph-based circuit description called Galois-field Arithmetic Circuit Graph (GF-ACG). First, we extend GF-ACG representation to describe GFs defined by normal basis in addition to polynomial basis. We then apply the extended design method to Massey-Omura parallel multipliers which are well known as typical multipliers based on normal basis. We present the formal description of the multipliers in a hierarchical manner and show that the verification time can be greatly reduced in comparison with those of the conventional techniques. In addition, we design GF exponentiation circuits consisting of the Massey-Omura parallel multipliers and an inversion circuit over composite field GF(((22)2)2) in order to demonstrate the advantages of normal-basis circuits over polynomial-basis ones.

This paper presents a new approach to designing arithmetic circuits by using a graph-based evolutionary optimization technique called Evolutionary Graph Generation (EGG). The key idea of the proposed method is to introduce a higher level of abstraction for arithmetic algorithms, in which arithmetic circuit structures are modeled as data-flow graphs associated with specific number representation systems. The EGG system employs evolutionary operations to transform the structure of graphs directly, which makes it possible to generate the desired circuit structure efficiently. The potential capability of EGG is demonstrated through an experiment of generating constant-coefficient multipliers.

Power supply noise waveforms within cryptographic VLSI circuits in a 65nm CMOS technology are captured by using an on-chip voltage waveform monitor (OCM). The waveforms exhibit the correlation of dynamic voltage drops to internal logical activities during Advance Encryption Standard (AES) processing, and causes side-channel information leakage regarding to secret key bytes. Correlation Power Analysis (CPA) is the method of an attack extracting such information leakage from the waveforms. The frequency components of power supply noise contributing the leakage are shown to be localized in an extremely low frequency region. The level of information leakage is strongly associated with the size of increment of dynamic voltage drops against the Hamming distance in the AES processing. The time window of significant importance where the leakage most likely happens is clearly designated within a single clock cycle in the final stage of AES processing. The on-chip power supply noise measurements unveil the facts about side-channel information leakage behind the traditional CPA with on-board sensing of power supply current through a resistor of 1 ohm.

This paper presents a glitchy-clock generator integrated in FPGA for evaluating fault injection attacks and their countermeasures on cryptographic modules. The proposed generator exploits clock management capabilities, which are common in modern FPGAs, to generate clock signal with temporal voltage spike. The shape and timing of the glitchy-clock cycle are configurable at run time. The proposed generator can be embedded in a single FPGA without any external instrument (e.g., a pulse generator and a variable power supply). Such integration enables reliable and reproducible fault injection experiments. In this paper, we examine the characteristics of the proposed generator through experiments on Side-channel Attack Standard Evaluation Board (SASEBO). The result shows that the timing of the glitches can be controlled at the step of about 0.17 ns. We also demonstrate its application to the safe-error attack against an RSA processor.

Electromagnetic analysis (EMA) against public-key cryptographic software on an embedded OS is presented in this paper. First, we propose a method for finding an observation point for EMA, where the EM radiation caused by cryptographic operations can be observed with low noise. The basic idea is to find specific EM radiation patterns produced by cryptographic operations given specific input pattern. During the operations, we scan the surface of the target device(s) with a micro magnetic probe. The scan is optimized in advanced using another compatible device that has the same central processing unit (CPU) and OS as the target device. We demonstrate the validity of the proposed EMAs through some EMA experiments with two types of RSA software on an embedded OS platform. The two types of RSA software have different implementations for modular multiplication algorithms: one is a typical and ready-made implementation using BigInteger class on Java standard library, and another is a custom-made implementation based on the Montgomery multiplication algorithm. We conduct experiments of chosen-message EMA using our scanning method, and show such EMAs successfully reveal the secret key of RSA software even under the noisy condition of the embedded OS platform. We also discuss some countermeasures against the above EMAs.

This study presents a formal verification method for Galois-field (GF) arithmetic circuits with the characteristics of more than two values. The proposed method formally verifies the correctness of circuit functionality (i.e., the input-output relations given as GF-polynomials) by checking the equivalence between a specification and a gate-level netlist. We represent a netlist using simultaneous algebraic equations and solve them based on a novel polynomial reduction method that can be efficiently applied to arithmetic over extension fields $mathbb{F}_{p^m}$, where the characteristic p is larger than two. By using the reverse topological term order to derive the Gröbner basis, our method can complete the verification, even when a target circuit includes bugs. In addition, we introduce an extension of the Galois-Field binary moment diagrams to perform the polynomial reductions faster. Our experimental results show that the proposed method can efficiently verify practical $mathbb{F}_{p^m}$ arithmetic circuits, including those used in modern cryptography. Moreover, we demonstrate that the extended polynomial reduction technique can enable verification that is up to approximately five times faster than the original one.

This paper presents a formal design of arithmetic circuits using an arithmetic description language called ARITH. The key idea in ARITH is to describe arithmetic algorithms directly with high-level mathematical objects (i.e., number representation systems and arithmetic operations/formulae). Using ARITH, we can provide formal description of arithmetic algorithms including those using unconventional number systems. In addition, the described arithmetic algorithms can be formally verified by equivalence checking with formula manipulations. The verified ARITH descriptions are easily translated into the equivalent HDL descriptions. In this paper, we also present an application of ARITH to an arithmetic module generator, which supports a variety of hardware algorithms for 2-operand adders, multi-operand adders, multipliers, constant-coefficient multipliers and multiply accumulators. The language processing system of ARITH incorporated in the generator verifies the correctness of ARITH descriptions in a formal method. As a result, we can obtain highly-reliable arithmetic modules whose functions are completely verified at the algorithm level.

We introduce PC Linux cluster computing techniques to an Evolutionary Graph Generation (EGG) system, and successfully implement the parallel version of the EGG system, called PEGG. Our survey satisfactorily shows that the parallel evolutionary approach meets our expectation that the final solutions obtained from PEGG will be as good as or better than those obtained from EGG, and that PEGG can ultimately improve the speed of evolution.

This paper presents an algorithm-level interpretation of fast adder structures in binary/multiple-valued logic. The key idea is to employ a unified representation of addition algorithms called Counter Tree Diagrams (CTDs). The use of CTDs makes it possible to describe and analyze addition algorithms at various levels of abstraction. A high-level CTD represents a network of coarse-grained components associated with multiple-valued logic devices, while a low-level CTD represents a network of primitive components directly mapped onto binary logic devices. The level of abstraction in circuit representation can be changed by decomposition of CTDs. We can derive possible variations of adder structures by decomposing a high-level CTD into low-level CTDs. This paper demonstrates the interpretation of redundant arithmetic adders based on CTDs. We first introduce an extension of CTDs to represent possible redundant arithmetic adders with limited carry propagation. Using the extended version of CTDs, we can classify the conventional adder structures including those using emerging devices into three types in a systematic way.

This paper proposes a multiple-fault injection attack based on adaptive control of fault injection timing in embedded microcontrollers. The proposed method can be conducted under the black-box condition that the detailed cryptographic software running on the target device is not known to attackers. In addition, the proposed method is non-invasive, without the depackaging required in previous works, since such adaptive fault injection is performed by precisely generating a clock glitch. We first describe the proposed method which injects two kinds of faults to obtain a faulty output available for differential fault analysis while avoiding a conditional branch in a typical recalculation-based countermeasure. We then show that the faulty output can be obtained by the proposed method without using information from the detailed instruction sequence. In particular, the validity of the proposed method is demonstrated through experiments on Advanced Encryption Standard (AES) software with a recalculation-based countermeasure on 8-bit and 32-bit microcontrollers. We also present a countermeasure resistant to the proposed method.

This paper presents an efficient graph-based evolutionary optimization technique called Evolutionary Graph Generation (EGG), and its application to the design of fast constant-coefficient multipliers using parallel counter-tree architecture. An important feature of EGG is its capability to handle the general graph structures directly in evolution process instead of encoding the graph structures into indirect representations, such as bit strings and trees. This paper also addresses the major problem of EGG regarding the significant computation time required for verifying the function of generated circuits. To solve this problem, a new functional verification technique for arithmetic circuits is proposed. It is demonstrated that the EGG system can create efficient multiplier structures which are comparable or superior to the known conventional designs.

This paper proposes an efficient scheme for concurrent error detection for hardware implementations of the block cipher AES. In the proposed scheme, the circuit component for the round function is divided into two stages, which are used alternately for encryption (or decryption) and error checking in a pipeline. The proposed scheme has a limited overhead with respect to size and speed for the following reasons. Firstly, the need for a double number of clock cycles is eliminated by virtue of the reduced critical path. Secondly, the scheme only requires minimal additional circuitry for error detection since the detection is performed by the remaining encryption (or decryption) components within the pipeline. AES hardware with the proposed scheme was designed and synthesized by using 90-nm CMOS standard cell library with various constraints. As a result, the proposed circuit achieved 1.66 Gbps @ 12.9 Kgates for the compact version and 4.22 Gbps @ 30.7 Kgates for the high-speed version. These performance characteristics are comparable to those of a basic AES circuit without error detection, where the overhead of the proposed scheme is estimated to be 14.5% at maximum. The proposed circuit was fabricated in the form of a chip, and its error detection performance was evaluated through experiments. The chip was tested with respect to fault injection by using clock glitch, and the proposed scheme successfully detected and reacted to all introduced errors.

This paper explores the feasibility of power analysis attacks against low-latency block ciphers implemented with unrolled architectures capable of encryption/decryption in a single clock cycle. Unrolled architectures have been expected to be somewhat resistant against side-channel attacks compared to typical loop architectures because of no memory (i.e. register) element storing intermediate results in a synchronous manner. In this paper, we present a systematic method for selecting Points-of-Interest for power analysis on unrolled architectures as well as calculating dynamic power consumption at a target function. Then, we apply the proposed method to PRINCE, which is known as one of the most efficient low-latency ciphers, and evaluate its validity with an experiment using a set of unrolled PRINCE processors implemented on an FPGA. Finally, a countermeasure against such analysis is discussed.

With the rising importance of information security, the necessity of implementing better security measures in the physical layer as well as the upper layers is becoming increasing apparent. Given the development of more accurate and less expensive measurement devices, high-performance computers, and larger storage devices, the threat of advanced attacks at the physical level has expanded from the military and governmental spheres to commercial products. In this paper, we review the issue of information security degradation through electromagnetic (EM)-based compromising of security measures in the physical layer (i.e., EM information security). Owing to the invisibility of EM radiation, such attacks can be serious threats. We first introduce the mechanism of information leakage through EM radiation and interference and then present possible countermeasures. Finally, we explain the latest research and standardization trends related to EM information security.

This paper presents an automatic hierarchical formal verification method for arithmetic circuits over Galois fields (GFs) which are dedicated digital circuits for GF arithmetic operations used in cryptographic processors. The proposed verification method is based on a combination of a word-level computer algebra procedure with a bit-level PPRM (Positive Polarity Reed-Muller) expansion procedure. While the application of the proposed verification method is not limited to cryptographic processors, these processors are our important targets because complicated implementation techniques, such as field conversions, are frequently used for side-channel resistant, compact and low power design. In the proposed method, the correctness of entire datapath is verified over GF(2m) level, or word-level. A datapath implementation is represented hierarchically as a set of components' functional descriptions over GF(2m) and their wiring connections. We verify that the implementation satisfies a given total-functional specification over GF(2m), by using an automatic algebraic method based on the Gröbner basis and a polynomial reduction. Then, in order to verify whether each component circuit is correctly implemented by combination of GF(2) operations, i.e. logic gates in bit-level, we use our fast PPRM expansion procedure which is customized for handling large-scale Boolean expressions with many variables. We have applied the proposed method to a complicated AES (Advanced Encryption Standard) circuit with a masking countermeasure against side-channel attack. The results show that the proposed method can verify such practical circuit automatically within 4 minutes, while any single conventional verification methods fail within a day or even more.

This paper presents a unified representation of fast addition algorithms based on Counter Tree Diagrams (CTDs). By using CTDs, we can describe and analyze various adder architectures in a systematic way without using specific knowledge about underlying arithmetic algorithms. Examples of adder architectures that can be handled by CTDs include Redundant-Binary (RB) adders, Signed-Digit (SD) adders, Positive-Digit (PD) adders, carry-save adders, parallel counters (e.g., 3-2 counters and 4-2 counters) and networks of such basic adders/counters. This paper also discusses the CTD-based analysis of carry-propagation-free adders using various number representations.

This paper proposes a constant-power adder based on multiple-valued logic and its application to cryptographic processors being resistant to side-channel attacks. The proposed adder is implemented in Multiple-Valued Current-Mode Logic (MV-CML). The important feature of MV-CML is that the power consumption can be constant regardless of input values, which makes it possible to prevent power-analysis attacks using dependencies between power consumption and intermediate values or operations of the executed cryptographic algorithms. In this paper, we focus on a multiple-valued Binary Carry-Save adder based on the Positive-Digit (PD) number system and its application to RSA processors. The power characteristic of the proposed design is evaluated with HSPICE simulation using 90 nm process technology. The result shows that the proposed design can achieve constant power consumption with lower performance overhead in comparison with the conventional binary design.

This paper presents an efficient method for differential fault analysis (DFA) on substitution-permutation network (SPN)-based block ciphers. A combination of a permutation cancellation and an algebraic key filtering technique makes it possible to reduce the computational cost of key filtering significantly and therefore perform DFAs with new fault models injected at an earlier round, which defeats conventional countermeasures duplicating or recalculating the rounds of interest. In this paper, we apply the proposed DFA to the LED block cipher. Whereas existing DFAs employ fault models injected at the 30th round, the proposed DFA first employs a fault model injected at the 29th round. We demonstrate that the proposed DFA can obtain the key candidates with only one pair of correct and faulty ciphertexts in about 2.1h even from the 29th round fault model and the resulting key space is reduced to 24.04