PROOFS 2017: Papers with Abstracts

Abstract. The security of embedded systems can be dramatically improved through the use of formally verified isolation mechanisms such as separation kernels, hypervisors, or microkernels. For trustworthiness, particularly for system level behaviour, the verifications need precise models of the underlying hardware. Such models are hard to attain, highly complex, and proofs of their security properties may not easily apply to similar but different platforms. This may render verification economically infeasible.

To address these issues, we propose a compositional top-down approach to embedded system specification and verification, where the system-on-chip is modeled as a network of distributed automata communicating via paired synchronous message passing. Using abstract specifications for each component allows to delay the development of detailed models for cores, devices, etc., while still being able to verify high level security properties like integrity and confidentiality, and soundly refine the result for different instantiations of the abstract components at a later stage.

As a case study, we apply this methodology to the verification of information flow security for an industry scale security-oriented hypervisor on the ARMv8-A platform. The hypervisor statically assigns (multiple) cores to each guest system and implements a rudimentary, but usable, inter guest communication discipline. We have completed a pen-and-paper security proof for the hypervisor down to state transition level and report on a partially completed verification of guest mode security in the HOL4 theorem prover.

Abstract. Masking is a popular countermeasure against side-channel attacks, that randomizes secret data with random and uniform variables called masks. At software level, masking is usually added in the source code and its effectiveness needs to be verified. In this paper, we propose a symbolic method to verify side-channel robustness of masked programs. The analysis is performed at the assembly level since compilation and optimizations may alter the added protections. Our proposed method aims to verify that intermediate computations are statistically independent from secret variables using defined distribution inference rules. We verify the first round of a masked AES in 22s and show that some secure algorithms or source codes are not leakage-free in their assembly implementations.

Abstract. Horizontal collision correlation analysis (HCCA) imposes a serious threat to
simple power analysis resistant elliptic curve cryptosystems involving unified algorithms, for e.g. Edward curve unified formula. This attack can be mounted even in presence of differential power analysis resistant randomization schemes. In this paper we have designed an effective countermeasure for HCCA protection, where the dependency of side-channel leakage from a school-book multiplication with the underling multiplier operands is investigated. We have shown how changing the sequence in which the operands are passed to the multiplication algorithm introduces dissimilarity in the information leakage. This disparity has been utilized in constructing a zero-cost countermeasure against HCCA. This countermeasure has been shown to help in HCCA resistivity. Additionally we provide experimental validation for our proposed countermeasure technique on a SASEBO platform. To the best of our knowledge, this is the first time that asymmetry in information leakage has been utilized in designing a side channel countermeasure and successfully applied in an ECC-based crypto-module.

Abstract. Characterization of all possible faults in a cryptosystem exploitable for fault attacks is a problem which is of both theoretical and practical interest for the cryptographic community. The complete knowledge of exploitable fault space is desirable while designing optimal countermeasures for any given crypto-
implementation. In this paper, we address the exploitable fault characterization problem in the context of Differential Fault Analysis (DFA) attacks on block ciphers. The formidable size of the fault spaces demands an automated albeit fast mechanism for verifying each individual fault instance and neither the
traditional, cipher-specific, manual DFA techniques nor the generic and automated Algebraic Fault Attacks (AFA) [10] fulfill these criteria. Further, the diversified structures of different block ciphers suggest that such an automation should be equally applicable to any block cipher. This work presents an automated
framework for DFA identification, fulfilling all aforementioned criteria, which, instead of performing the attack just estimates the attack complexity for each individual fault instance. A generic and extendable data-mining assisted dynamic analysis framework capable of capturing a large class of DFA distinguishers
is devised, along with a graph-based complexity analysis scheme. The framework significantly outperforms another recently proposed one [6], in terms of attack class coverage and automation effort. Experimental evaluation on AES and PRESENT establishes the effectiveness of the proposed framework in detecting
most of the known DFAs, which eventually enables the characterization of the exploitable fault space.

Abstract. In a novel analysis, we show that arbitrarily many Arbiter PUFs can be combined into a stable XOR Arbiter PUF. To the best of our knowledge, this design cannot be modeled by any known oracle access attack in polynomial time.

Using majority vote of Arbiter Chain responses, our analysis shows that with a polynomial number of votes the XOR Arbiter PUF stability of almost all challenges can be boosted exponentially close to 1; that is, the stability gain through majority voting can exceed the stability loss introduced by large XORs for a feasible number of votes. Hence, our proposal enables the designer to increase the attacker's effort exponentially while still maintaining polynomial design effort for all known oracle access modeling attacks. This is the first result that relates PUF design to this traditional cryptographic design principle.