Name
Abstract | ||
|---|---|---|
The complexity level of hardware design has increased extensively, and consequently it became subject of errors. That's why it is extremely important to verify the correctness of designs, especially in critical systems like those of security.
The problem is that the typical Hardware Description Languages (HDLs) like VHDL and Verilog are made mostly for description and simulation purposes; however, the simulation is insufficient validation technique in complex designs such as the cryptographic circuits. Thus, formal verification has become an important technique towards establishing the correctness of hardware designs; nonetheless it still faces many challenges; which make it a worth-while research problem.
This paper presents an approach to formally verify the cryptographic circuits. It consists of using a purely functional framework namely Haskell to describe both the behavioral and structural descriptions. In addition, such approach relies on the use of hierarchy and modularity techniques in order to reduce the design complexity, and hence simplify the verification task. Last but not least we use Lava which is an HDL embedded into Haskell that allows checking automatically the safety and equivalence properties of circuits in several ways.
To show the potential features of the proposed approach, we applied it to the Data Encryption Standard (DES) circuit, which is a symmetric block cipher. Thereafter, a methodological design approach for the verification of the design implementation against the specification is presented.
|
Year | DOI | Venue |
|---|---|---|
2019 | 10.1145/3320326.3320367 | Proceedings of the 2nd International Conference on Networking, Information Systems & Security |
Keywords | DocType | ISBN |
Cryptographic circuit, Data Encryption Standard, Formal verification, Functional language, Hardware Description Language, Hardware verification, Lava, Symmetric cipher | Conference | 978-1-4503-6645-8 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Abir Bitat | 1 | 0 | 0.34 |
| Salah merniz | 2 | 0 | 0.34 |