Cryptol experience

50 %
50 %
Information about Cryptol experience
Technology

Published on July 28, 2009

Author: UlissesCosta

Source: slideshare.net

Description

The last milestone from our Formal Methods MSc project.

The Cryptol Experience Pedro Pereira Ulisses Costa Formal Methods in Software Engineering July 27, 2009 Pedro Pereira, Ulisses Costa The Cryptol Experience

Last milestone’s recap! We showed you Cryptol → VHDL translation Hardware performance analysis Real application of the verification framework Pedro Pereira, Ulisses Costa The Cryptol Experience

Electronic Design Automation with Cryptol 1 Write Cryptol specification closely resembling the mathematical one 2 Convert top-level function into stream model for performance analysis 3 Substitute unsupported constructs for compilation 4 Use verification framework for safety and equivalence checking 5 Adjust implementation according to space and time requirements Pedro Pereira, Ulisses Costa The Cryptol Experience

Milestone I We had to Learn the Cryptol language Create a SNOW 3G specification We consulted SNOW 3G specification Programming guide Examples folder Pedro Pereira, Ulisses Costa The Cryptol Experience

Milestone I Overall SNOW 3G is composed of simple manipulations and has a strong mathematical structure Clear and compact functional specification in Cryptol Quick specification process Pedro Pereira, Ulisses Costa The Cryptol Experience

Milestone I Programming guide Well written Cryptol definitions could be displayed in a different style Block cipher operation modes? Examples Great for watching Cryptol in action Perhaps two different specification-oriented case studies Pedro Pereira, Ulisses Costa The Cryptol Experience

Milestone II We had to Generate an efficient and equivalent C implementation We consulted Tools user guide Pragmatic Equivalence and Safety Checking in Cryptol Pedro Pereira, Ulisses Costa The Cryptol Experience

Milestone II Overall We didn’t quite grasp the difference between SBV and C Optimizations? We learned a lot about the verification framework Pedro Pereira, Ulisses Costa The Cryptol Experience

Milestone II Tools user guide Lacks some information regarding interpreter modes and respective differences Could use better formatting in some sections PESCC Contains everything needed to know about the verification framework Maybe not suitable/relevant for the end-user Pedro Pereira, Ulisses Costa The Cryptol Experience

Milestone III We had to Generate an efficient and equivalent VHDL implementation We consulted FPGA tutorial Pedro Pereira, Ulisses Costa The Cryptol Experience

Milestone III Opinions :help <options> FPGA tutorial also lacks a more consistent formatting Some information could have gone to the tools user guide We learned a lot about EDA but... Pedro Pereira, Ulisses Costa The Cryptol Experience

As promissed! MULxPOW MULxPOW : ([8] , [8] , [8]) -> [8]; MULxPOW (v ,i , c ) = res @ i where res = [ v ] # [| MULx (e , c ) || e <- res |]; The latency of this implementation is 28 , because Cryptol needs the static latency ⇒ latency of this circuit is equal to the worst-case latency But the third parameter is always the same and the second one only instantiates 8 possible values We can be more efficient by implementing it as 8 static lookup tables with 256 8-bit elements each ⇒ BlockRAMs Pedro Pereira, Ulisses Costa The Cryptol Experience

Even better DIVα and MULα are responsible for updating the LFSR 2 static lookup tables with 256 32-bit elements each! Pedro Pereira, Ulisses Costa The Cryptol Experience

SPIR Report === Summary of Path Timing Estimates === Overall clock period: 8.38 ns (119.3 MHz ) Input pin to flip-flop: 1.94 ns (514.7 MHz ) Flip-flop to flip-flop: 7.72 ns (129.6 MHz ) Flip-flop to output pin: 8.38 ns (119.3 MHz ) Input pin to output pin: No paths === Summary of Size Estimates === Estimated total size: about 6848 LUTs , 2776 Flipflops === Circuit Timing === circuit latency: 37 cycles (36 cycles plus propagation delay ) circuit rate: one element per cycle output length: unbounded total time: unbounded Pedro Pereira, Ulisses Costa The Cryptol Experience

Pipelining? reg pragma Sequential circuits in the stream model can be pipelined Separation of a function into several smaller computational units Each unit is a stage in the pipeline consuming output from previous stage and producing output to the next Can increase clockrate and throughput Pedro Pereira, Ulisses Costa The Cryptol Experience

Pipelining! Timing Summary: Minimum period: 6.214 ns (Maximum Frequency: 160.930 MHz) Minimum input arrival time before clock: 2.892 ns Maximum output required time after clock: 11.497 ns Maximum combinational path delay: No path found Device Utilization (size summary): Number of Slices: 1212 out of 14752 8% Number of Slice Flip Flops: 1810 out of 29504 6% Number of 4 input LUTs: 2192 out of 29504 7% Pedro Pereira, Ulisses Costa The Cryptol Experience

Comparison Implementation Frequency (MHz) Throughput (Mbps) Proposed SNOW 3G 160 5120 SNOW 3G 249 7968 SNOW 3G 100 2500 SNOW 2.0 141 4512 SNOW 1.0 66.5 2128 Pedro Pereira, Ulisses Costa The Cryptol Experience

The Big Question We claim that non-hardware people can get good results by working in Cryptol and would like to confirm or deny that claim. Galois, Inc. Yes, we can! Pedro Pereira, Ulisses Costa The Cryptol Experience

(Other) Questions ? Pedro Pereira, Ulisses Costa The Cryptol Experience

Add a comment

Related presentations

Presentación que realice en el Evento Nacional de Gobierno Abierto, realizado los ...

In this presentation we will describe our experience developing with a highly dyna...

Presentation to the LITA Forum 7th November 2014 Albuquerque, NM

Un recorrido por los cambios que nos generará el wearabletech en el futuro

Um paralelo entre as novidades & mercado em Wearable Computing e Tecnologias Assis...

Microsoft finally joins the smartwatch and fitness tracker game by introducing the...

Related pages

Home DE - CrypTool Portal

Was ist CrypTool 1? CrypTool 1 (CT1) ist ein Open-Source-Programm für Kryptographie und Kryptoanalyse. Es ist die verbreiteste E-Learning-Software ihrer Art.
Read more

CrypTool 2 - CrypTool Portal

CRYPTOOL 1; CRYPTOOL 2; JCRYPTOOL; CRYPTOOL ONLINE; ... providing a consistent and rich user experience. ... CrypTool 2 is licensed under the Apache Open ...
Read more

Case Studies in Cryptol - Chalmers Publication Library (CPL)

Case Studies in Cryptol A study of domain specific languages for DSP ... The proposals are based on experience gained from case studies and study of
Read more

Cryptol, a DSL for cryptographic algorithms

Cryptol is a domain-specific functional language designed by Galois, Inc in collaboration with the the NSA for specifying cryptographic algorithms.
Read more

Soaring price of Bitcoin prompts CryptoLocker ransomware ...

Soaring price of Bitcoin prompts CryptoLocker ransomware price break CryptoLocker operators may be ruthless, but they don't lack business smarts.
Read more

Cryptography Intern job at CloudFlare in San Francisco, CA ...

Please contact support@jobscore.com if you need further ... Experience in the theory and implementation of ... Experience with the cryptol ...
Read more

CrypTool: experiment with cryptographic algorithms ...

CrypTool is a free learning software for Windows and other operating systems offers information about and visualizations of cryptographic ...
Read more

Cryptol - privacypolicy

Cryptol. Home; Downloads; Documentation; Verification; ... We also use Personal Information to customize and improve your user experience on the Managed Site.
Read more