Cryptographic circuits have become indispensable in most systems where security is the main criteria. That is why it is important to verify the correctness of their design. In this paper we propose a formal methodology for design and verification of the cryptographic circuits; it combines two techniques, the SAT Solver technique, which is automatic and has been used to verify the correctness of combinational logic parts; and, the induction technique, which has been used for sequential logic parts. The proposed approach consists of using the functional Hardware Description Language (HDL) Lava to describe both behavioural and structural aspects of a circuit; using Finite State Machines (FSMs). And then to verify the specification and check the equivalence of the implementation against it, in order to prove the circuit's correctness. To show the features of the proposed approach, it was applied to verify implementations of both sequential and pipelined architectures of the symmetric block cipher AES (Advanced Encryption Standard).
Nowadays networks are trusted with extremely sensitive information; hence the importance of cryptography which makes its security possible. As a consequence, cryptographic co-processors have become indispensable in many modern applications. A co-processor is a hardware module that adds functions to a standard CPU; a cryptographic one adds cryptographic IP cores specialized for encryption and decryption operations. Due to the sensitivity of the security matter; it is important to design and implement these circuits correctly.
Circuits design process goes through several steps; the first one consists in converting the informal description of the design to an algorithmic specification. From this latter, a microarchitectural implementation is derived through refinement; followed by a series of design steps reducing the abstraction levels until a realizable description is obtained. After each of these design steps; a verification process is performed.
Design verification of hardware can either concern non functional aspects like time, power and layout, or functional verification; this latter, consists in checking that the structural implementation provides the same behavior mentioned in the behavioral specification; which can be done in quite a few ways, such as simulation, formal proof, and semi-formal verification in which the former techniques are combined.
In this work, we use formal methods in order to design and verify the cryptographic circuits through functional verification. In section 2 we discuss related literature. In section 3, we explain our design and verification methodology. In section 4, we demonstrate how we applied our approach in order to verify sequential and pipelined architectures of the symmetric cryptographic circuit AES. And finally conclusions are drawn in section 5.
Imperative HDLs like VHDL and verilog, are still the most used for describing digital circuits. Therefore, the majority of the existing similar works are based on using them [1], [2], [3], [4], [5]. These languages are intended for description, simulation and synthesis of hardware; but not for formal verification due to their lack of formal semantics; in addition, they do not allow descriptions of the highest levels of design. As a consequence, most of the mentioned works use the simulation technique [2], [3], [4], which is not suficient for critical systems such as the cryptographic circuits because it does not guarantee the absence of errors. It is possible to use formal verification on circuits described with imperatives HDLs, but with a great deal of dificulties; the behavioral specification that hides all implementation details therefore needs more powerful abstraction and structuring mechanisms [5]. For the verification of such complex circuits, deductive methods were used [1]; which is quite dificult, because it requires user guidance through all the verification process. Symbolic computation was used for the verification of cryptographic circuits in some algebraic approaches [ 6], [7]; similarly to the work presented herein, they use the hierarchy technique in order to reduce the complexity of design and therefore simplify the verification task. Equivalence checking and completion functions were used in a formal approach [8] for the verification of RTL descriptions in imperative HDL VHDL. A language and tool that support automated formal verification of cryptographic assembly code was proposed in [9]. As for the pipelined implementations of cryptographic circuits; the imperative HDL VHDL was used for the description and simulation of some cryptoprocessors in [10]; and formal verification was applied, but no details about the method that was used were mentioned.
Even though there exists several functional approaches that were applied for the verification of digital circuits; to the best of our knowledge; beside the work presented herein, there is only one approach for the implementation and verification of cryptographic circuits [ 11]. However; this approach uses the functional language only for the behavioral specification; but it uses an imperative HDL for the structural implementation; which brings back some translation dificulties between the two descriptions.
The design process of a circuit is divided into several steps, where the implementation resulting on a certain abstraction level is used as the specification on the next lower one. A verification phase is mandatory after each step, to avoid the propagation of errors between the abstraction levels. Therefore, in order to verify the correctness of a certain implementation, it is suficient to compare it to its already verified specification. The most challenging verification step is that of the highest levels of abstraction; this dificulty is caused by the gap between descriptions as the majority of HDLs don’t allow ones at those levels.
In this work, we propose a methodology of formal design and verification for the cryptographic circuits, we target the higher levels of abstraction, and we verify that the microarchitectural description of a cryptographic circuit is equivalent to the algorithmic one.
The other attribute of our proposed approach is that we use the functional language Haskell and its embedded HDL Lava to describe the circuits. This choice is motivated by their interesting characteristics such as: having formal descriptions that can be reasoned about; the composition of functions in the same way that complex circuits are composed; having much more concise descriptions, which makes finding errors easier; and last but not least, Lava has some incorporated tools for formal verification of circuits; which in our knowledge have never been used for the verification of the cryptographic circuits.
A FSMD (Finite State Machine with Datapath) model provides a systematic approach for designing sequential circuits; it combines a controller, modeled as a FSM, and a dapapath. We model both descriptions of the circuit (behavioral and structural) as FSMs.
A FSM in Haskell is a recursive function fsm, which represents the output function; it takes as input a − 1 with the next state function called step, like shown in the following form: = ( − 1) ℎ
=
Since the two descriptions are at diferent levels of abstraction, they deal with diferent types
of data; therefore, a mapping function abs is needed between the two them. Thus, in order to
verify the implementation; the following theorem must be proved:
∀ ∈ , ( ) = ( )
(
The proof of this theorem must be decomposed. Since both descriptions are hierarchical, we need to start by verifying the simplest components at the lowest level of hierarchy. Once they are verified, the verification of the upper components that they compose becomes possible.
The combinational parts of the implementation can be verified automatically using the SAT solver tool of Lava. As for the sequential parts; we use induction and equational reasoning.
When performing equivalence checking using SAT solvers, if the two descriptions are equivalents, the output of the Xor gate should be always False. If the output becomes True for any input sequence, it means that the SAT solver found a satisfiable assignment, which implies that the descriptions are producing diferent outputs for the same input.
In order to verify that two descriptions are equivalent, we have to define a safety property that expresses their equivalence. A safety property states that some condition is always true. This property is also defined as a function in the following form: = ℎ 1 = 1 2 = 2 = 1 <==> 2 To verify this property we use the Lava function satzoo, which is a call to the satisfiability solver: .
Since we want to verify that a component implements correctly its specification (which works with a diferent data type); the equivalence property should be defined in the following way instead: = Now, for the verification of the sequential part, which is the FSM it self, meaning the implementation of the whole circuit; we use induction like we mentioned previously. So, we start by verifying the base case (a); then we prove (b) that if the property holds for a step n; then it should hold for the following step n-1.
() 0 ( ) = ( 0 ) () ( ) = ( ) ⇒
( − 1) ( ) = ( ( − 1) )
The proposed approach for verifying both sequential and pipelined architectures is
summarized in Fig.1. We start by checking if the behavioural description of the sequential architecture
holds the verification property (
We prove the verification property (
Advanced Encryption Standard (AES) [14] is a symmetric block cipher, constructed based on the Rijandael system; it encrypts blocks of 128 bits using a key of 128 bits size, 129, or 256 bits depending on the system’s version. We demonstrate our proposed approach on AES128.
The encryption consists of ten identical rounds of processing; each of which includes four steps: sub bytes, shift rows, mix columns and add key; except for the last one, where the mix columns function is not performed. The decryption on the other hand, uses the inverse of these functions in a diferent order.
The key expansion function uses the cipher key to produce sub-keys in the same number of rounds. In this work, we pre-calculate the sub-keys in advance.
The basic hardware architecture used to implement an encryption or decryption unit of the symmetric AES cipher is shown in Fig.3. This architecture characteristics is that only one block of data is encrypted at a time.
The AES core is composed of three units: encryption unit, decryption unit, and key expansion unit in order to pre-calculate the sub-keys. It is defined by the function seqSpecAES, which takes as inputs a text text, a key key and the operation type op.
(, , ) = ℎ = 10 = ( == 1) ℎ ((, )) ((, )) The function seqSpecEnc converts the text from ascii to hexadecimal, and decomposes it into blocks of 128bits, and send them sequentially to the function that encrypts one block of data. The behavioral description of this encryption unit is expressed as a FSM in Lava, represented by the recursive function seqSpecEncFSM, which takes as input the stat which is composed of: the round number n, one block of the plain text pt, the current cipher text ct, and the pre-calculated sets of sub-keys keys; and it calculates the round cipher text using the next state function stepSeqSpecEnc.
(, , , ) = (( − 1), , , ) ℎ = ( == 10) = ( == 1) = (, ( (!!0) , ), ) = (, , !!(10 − ( − 1)))
(, , , ) = (( − 1), , , ) = ( == 10) = (, , !!( − 1)) (, , ) = ( ) = (, (, ((ℎ ))) , ((, ((ℎ )))))
The hardware implementation of AES is described in the same hierarchical way as the behavioral description; it is composed of three components : the key expansion function keyExpansionI, the encryption function seqImpEnc, and the decryption function seqImpDec. (, , ) = = 10 = ( == 1) ℎ ((, )) ( (, ))
The encryption function seqImpEnc converts the text from ascii to hexadecimal to binary and decompose it into blocks of 128bits and send it sequentially block by block to the function seqImpEncFSM, which is the FSM that models the structural description of the encryption unit. (, , , ) = (( − 1), , , ) = (, , !!( − 1)) (, , ) = ( )
The inner components of this circuit (seqImpEncFSM), like muxI, addKeyI... are defined in terms of their structure using gates, unlike the muxS, addKeyS... which express the behavior of that component.
(, , ) = ℎ (, , ) = ( ) ( ( ) ) The hardware implementations of the main four components of AES are the followings: – Add Key: is implemented using the bitwise XOR gate; and therefore it is the inverse of itself. – Shift Rows: is a left cyclic shift of bits. The inverse shift rows is a right cyclic shift. – Sub Bytes: relies on operations in the Galois Field GF (28); it can be implemented using only logic i.e. implementing circuits for the multiplication operation, the inverse operation, and for the afine transformation operation; or using the S-boxes, or Look-Up-Tables (LUTs); which are implemented as Read Only Memories (ROMs). We need 16 8x8 bit ROMs for the encryption and 16 for the Inverse Sub Bytes. – Mix Columns: relies on operations in GF(28) as well, and can be expressed using only logic or LUTs too; which are implemented as 8x8 bit ROMs for each of the multiplication operations of both encryption and decryption process.
seqImpDecFSM function represents the structural description of the decryption unit.
There are several architectures possible for pipelined block ciphers [15] ; we chose the one with inner-round pipelining depicted in Fig.4. with four pipeline stages. This makes it possible to encrypt four blocks simultaneously.
Similarly to the sequential architecture; AES is composed of three units: encryption, decryption, and key expansion. This latter is the same as in the sequential architecture. (, , ) = ℎ = 10 = ( == 1) ℎ ((, )) ((, )) The function pipeSpecEnc converts the text from ascii to hexadecimal, decomposes it into blocks of 128bits, and send them to the function pipeSpecEncFSM that encrypts four blocks of data. Unlike in the sequential architecture, where the number of states equals the number of rounds; in this architecture, more internal states appear; which represents the pipeline stages registers. Thus, the next-state function stepPipeSpecEnc is a recursive function that takes as input the number of internal step n, the pre-calculated keys keys, and the current state of the four stages registers (c1,c2,c3,c4). (4, ) = 4 ℎ = (ℎ (((4!!0, (!!0))))) = ℎ (((4!!1, (!!0)))) = (3 = (4!!2, (!!0))) = (4!!3, (!!0)) (, (1, 2, 3, 4), ) = (34, (, , , ), ) 1 = ((!!10), 3) 2 = ((!!10), (ℎ 2)) 3 = ((!!10), ℎ ( 1)) 4 = ((!!10), (ℎ ((((!!9), 4))))) 4 = [1, 2, 3, 4] (, (, , , ), ) = (( − 1), (, , , ), ) ℎ = ℎ = = ℎ = = (, )
The decryption function pipeSpecDecFSM is also a FSM; it’s next-state function is stepPipeSpecDec.
Like for the sequential architecture, the hardware implementation of pipelined AES is described in the same hierarchical way as its behavioral description; it is composed of three components : the key expansion function keyExpansionI, the encryption function pipeImpEnc, and the decryption function pipeImpDec.
(, , ) =
The encryption function PipeImpEnc converts the text from ascii to hexadecimal to binary and decompose it into blocks of 128bits and send them to the function pipeImpEncFSM, which is the FSM that models the structural description of the encryption unit. (4, ) = 4 = ℎ (((4!!1, (!!0)))) = ((4!!2, (!!0))) = (4!!3, (!!0)) (, (1, 2, 3, 4), ) = (34, (4, , , ), ) 1 = ((!!10), 3) 2 = ((!!10), (ℎ 2)) 3 = ((!!10), (ℎ (1))) 4 = ((!!10), (ℎ ((((!!9), 4))))) 4 = [1, 2, 3, 4] (, (, , , ), ) = (( − 1), (, , , ), )
The pipeImpDecFSM function represents the decryption FSM; it’s next-state function is stepPipeImpDec.
In order to verify that both sequential and pipelined architectures implement correctly the behavior of their specifications; seven theorems have to be proved.
1. First we need to verify the correctness property of the initial specification, which is
expressed by the following theorem:
∀ , ( ) =
(
Theorem (
Because lists are infinite structures, we need to define a verification property that is explicit about the sizes: = ( ) $ ∖ − > ( ) $ ∖ − >
(, )
To prove this property we call the satzoo function: 128 1408 (1408 is the total of eleven 128bit size keys); it returns Valid, which means that the specification holds that property. ( ) $ ∖ −
> 128
In order to be able to prove theorem (
All these properties were satisfied and gave back the answer implementations of these components are correct.
Valid; which means that the
The sub-circuit stepSeqImpEnc that is composed of the previously verified components is also correct according to the theorem proved above.
∀ , ( ) = ∀ , ℎ ( ) = ∀ , ( ) = ∀ , ( ) = ∀ , ( ) = (ℎ ), ( ), ( ), ( ), ⇒ ∀ , ( ) = ( )
( ),
Now that all the inner-components are verified, we verify the encryption FSM using induction. Basis: ((0, , , )) =
(0, , , ) ( (0, , , )) =
(0, , , ) ⇒
((0, , , )) = ( (0, , , )) Induction step: ∀ ∈ ; , ∈ [[[ ]]]; ∈ [[[[ ]]]]; ((, , , )) = ( (, , , )) ⇒ (((− 1), , , )) = ( ((− 1), , , )) ( (, , , )) = ( (( − 1), , , )) ℎ = ((, , , )) = (, , , ) = (( − 1), , , ) ℎ = ( ) ( ) = ( ) ⇒ = = (( − 1), , , ) = ((( − 1), , , )) ⇒ ((( − = ( (( − 1), , , )) 1), , , ))
We verified the correctness of the decryption unit’s implementation in the same way. ⇒ ∀ ∈ ; , ∈ [[[ ]]]; ∈ [[[[ ]]]]; ((, , , )) = ( (, , , )) ⇒ ∀ ∈ , , ∈ [ ℎ]; ((, , )) = ( (, , )) 4.3.2.
For the verification of the pipelined behavioral description against the sequential one, we verify the equivalence of their upper components that encrypts multiple blocks of data; because the next state in the sequential FSM consists of the result after one round; however, the next state in the pipelined FSM is the result of one inner-round pipeline stage. (, ) = ℎ = = 1 = (, ) 2 = (, ) = 1 <==> 2 ( ) $ ∖ − > ( ) $ ∖ − > (, )
=
We can only verify the property for a fixed text size at the time. (ℎ ) 128
For the implementation of the pipelined architecture, we check its equivalence to the behavioral description using induction. Since the inner components are the same for the sequential architecture we do not need to verify their equivalence. ∀ ∈ ; , , , ∈ [[[ ]]]]; ∈ [[[[ ]]]]; ( (, (, , , ), )) = ( (, (, , , ), )) ((0, (, , , ), )) = (0, (, , , ), ) ( (0, (, , , ), )) = (0, (, , , ), )
((0, (, , , ), )) = ( (0, (, , , ), )) Induction step: ∀ ∈ ; , , , , ∈ [[[ ]]], ∈ [[[[ ]]]]; ((, (, , , ), )) = ( (, (, , , ), )) ⇒ (((− 1), (, , , ), )) = ( ((− 1), (, , , ), )) ((, (, , , ), )) = ((, ( , , , ), )) = ((( − 1), (, , , ), )) ℎ = ( , ) = ( ) = ℎ ( ) = ( ) ( (, (, , , ), )) = ( (( − 1), (, , , ), )) ℎ = (, ) = = ℎ = ( , ) = ( (, )) ⇒ = ( ) = ( ) ⇒ = ℎ ( ) = (ℎ ) ⇒ = ( ) = ( ) ⇒ = ⇒ ((( − 1), (, , , ), )) = ((( − 1), ( , , , ), )) = ((( − 1), (, , , ), ) = ( (( − 1), (, , , ), )) ⇒ ∀ ∈ ; , , , , ∈ [[[ ]]], ∈ [[[[ ]]]]; ((, (, , , ), )) = ( (, (, , , ), ))
We verify the decryption unit in the same way as the encryption one. ∀ ∈ ; , , , , ∈ [[[ ]]], ∈ [[[[ ]]]]; ((, (, , , ), )) = ( (, (, , , ), ))
Now that we verified the equivalence between the pipelined step function’s implementation and its specification; the equivalence of the upper-components is verified. ∀ ∈ [[[[ ]]]], ∈ [[[[ ]]]]; ((, )) = ( (, )) ∀ ∈ [[[[ ]]]], ∈ [[[[ ]]]]; ((, )) = ( (, )) ⇒ ∀ ∈ , , ∈ [ℎ]; ((, , )) = ((, , ))
In table I, we show how long the verification process took for the main sub-components and
of the complete AES sequential circuit. As we can notice, all the theorems that has been proved
automatically using the Lava’s SAT solver, took less than 2s. As for theorems (
Table II shows the time that was taken for the verification of the AES pipelined circuit. Theorems (5) and (6), which express the equivalence between the specification of the sequential architecture and that of the pipelined one, where proved automatically using Lava’s SAT solver. As for the verification of the pipelined implementation against its verified specification, we proved theorems (7) and (8) using induction. This makes the total of the verification time for the pipelined circuit 421.97 s.
Finally, in table III, we recapitulate the diferent works related to the proposed approach. As we can see, the majority of the existing works are based on an imperative approaches. These approaches are well suited for simulation [2],[3], but we notice that it is still possible to use them for formal verification as well [1],[4],[5],[8],[9],[10]. In this case, the description for the design and verification is long and complex. Only one functional approach beside ours exists that targeted the cryptographic circuits [11]; no details about the verification time were mentioned. A couple of the existing works are based on an algebraic approach [6],[7]; similarly to our work, they use the hierarchy technique for proof decomposition; which makes the verification process easier. As we can see, our proposed methodology takes half the time for the verification of the same cryptographic circuit.
In this paper, we presented a formal design and verification methodology for symmetric cryptographic circuits. We combine the two techniques (induction and SAT solver) for verifying diferent parts of the implementation. The proposed approach was demonstrated over both sequential and pipelined architectures of the symmetric cipher AES128. As prospects, we aim to optimize the methodology into a fully automtic one, and to be able to design and verify the
Cryptographic circuit Imperative Imperative Imperative Imperative Functional Imperative Algebraic Algebraic Imperative Imperative Imperative Functional Functional
Formal methods Formal methods/simulation Theorem proving Equivalence checking Formal methods Equivalence checking Formal methods Formal methods Simulation Simulation Formal methods Formal methods Formal methods
DES AES128 SHA1 Pipelined KASUMI AES128 Pipelined KASUMI AES128 datapath AES128 AES256 TDES Pipelined AES128 Sequential AES128 Pipelined AES128 super-scalar architectures. [4] Lam, Chiu Hong. "Verification of pipelined ciphers". MS thesis. University of Waterloo, (2009). [5] Clarke, E., Kroening, D. "Hardware verification using ANSI-C programs as a reference". In Proceedings of the ASP-DAC Asia and South Pacific Design Automation Conference. pp. 308-311. IEEE. (2003). [6] Homma, Naofumi, Kazuya Saito, and Takafumi Aoki. "A Formal Approach to Designing Cryptographic Processors Based on (2) Arithmetic Circuits." IEEE Transactions on Information Forensics and Security vol. 7, no 1, p. 3-13. (2011). [7] Homma, Naofumi, Kazuya Saito, and Takafumi Aoki. "Toward formal design of practical cryptographic hardware based on Galois field arithmetic." IEEE Transactions on Computers. vol. 63, no 10, p. 2604-2613 (2013). [8] Lam, Chiu Hong, and Mark D. Aagaard. "Formal Verification of a Pipelined Cryptographic Circuit Using Equivalence Checking and Completion Functions." 2007 Canadian Conference on Electrical and Computer Engineering. IEEE, p. 1401-1404. (2007). [9] Bond, Barry, et al. "Vale: Verifying high-performance cryptographic assembly code." 26th
USENIX Security Symposium (USENIX Security 17). p. 917-934. (2017). [10] Kim, Ho Won, and Sunggu Lee. "Design and implementation of a private and public key crypto processor and its application to a security system." IEEE Transactions on Consumer Electronics.vol. 50, no 1, p. 214-224. (2004). [11] Lewis, Jef. "Cryptol: specification, implementation and verification of high-grade cryptographic applications." Proceedings of the 2007 ACM workshop on Formal methods in security engineering. p. 41-41.(2007). [12] Wolfs, Davy, et al. "Design automation for cryptographic hardware using functional languages." Proceedings of the 32nd WIC Symposium on Information Theory in the Benelux. Werkgemeenschap voor Informatie-en Communicatietheorie.; Netherlands, p. 194-201. (2011). [13] Guo, Xiaolong, et al. "Pre-silicon security verification and validation: A formal perspective."
Proceedings of the 52nd Annual Design Automation Conference. p. 1-6. (2015). [14] Daemen, Joan, and Vincent Rijmen. The design of Rijndael: AES-the advanced encryption standard. Springer Science and Business Media, (2013). [15] Gaj, K., and Chodowiec, P. (2009). FPGA and ASIC implementations of AES. In Cryptographic engineering (pp. 235-294). Springer, Boston, MA.