CaseStudiesInCryptol

Case Studies in Cryptol

Project assigned to Muhammad Asif with the following description:

The project is aimed to propose an extension to the Cryptol Language to make it useful for the DSP paradigm. Cryptol was invented to assist Cryptographers by providing a specialized way of specifying the Cryptographic protocols. We want to investigate the feasibility of specifying DSP algorithms in Cryptol by doing some case studies in DSP domains.

Following are tentative steps for the project:

Study Cryptol language and do programming exercises for practice. Study advanced features of Cryptol language to exploit it completely. It is required to analyze all features because we intend to propose an extension to Cryptol Language, to do that it is necessary to prove the current implementation is not sufficient.
Explore additional feature of Cryptol Toolset e.g. verification, code generation etc. Since it is important to verify the implementation as a proof for our correct implementations.
Research DSP area for most critical and widely used DSP algorithms (preferably with the help of someone who has worked in DSP). It is good to get a variety of algorithms for study because we want to cover most frequently used and effective features to implement.
Understand the DSP algorithms in terms of various ways they manipulate their input and build their outputs (it probably will be hard for me to understand what they actually achieve).
Write Cryptol specifications for DSP algorithms studied in the previous step and equivalence check them against standard implementations in C, VHDL or MATLAB.
Compare the implementation in Cryptol with existing implementation in C or MATLAB based on level of abstraction and ease of coding.
Study done in the previous step will be a basis for us to suggest how Cryptol can be extended to match the demands of typical DSP algorithms. Suitability of each extension will be influenced by how exhaustive case study we perform.
Implement one of proposed extensions as an embedded language in Haskell and verify its correctness using Quickcheck.

The above is based on the following proposal:

Cryptol is a domain specific language for the design of cryptographic algorithms, developed by Galois, Inc. It aims to support the unambiguous specification of cryptographic algorithms, to aid in testing and verification of such algorithms, and to enable safe and rapid retargetting to new hardware and software platforms.

With Ericsson, the Chalmers Functional Programming group is just starting a project to develop a domain specific language for Digital Signal Processing (DSP) algorithm design. We would like to raise the level of abstraction at which DSP algorithms are developed and implemented. Cryptol was part of the inspiration for this project. Therefore, as a first step, we would like to experiment with using Cryptol for DSP algorithm design. (This is also something that interests Galois, as they are interested in expanding the use of Cryptol into the larger DSP market.)

This project will implement some small and medium-sized DSP algorithms in Cryptol, and will summarise its strengths and weaknesses in this new domain. A result of the project will be proposals for how Cryptol should be extended to improve its applicablity in DSP. If of sufficiently high quality, this work will be suitable for publication as a paper in a workshop or conference.

Outline of project activities:

Learn the Cryptol langage.
Study DSP algoirhtms and choose suitable case studies, covering some typical aspects of DSP algorithms.
Perform those case studies.
Evaluate the result, for example by comparison with C or matlab.
Make suggestions for extensions to Cryptol that would make it more suitable for use in the DSP domain.
Prototype at least one of these extensions (probably directly as a DSL in Haskell).

Prerequisites: Functional programming, Programming paradigms or Programming languages, preferably some background in DSP; having taken Hardware description and verification is an advantage but is not a requirement. You should be interested both in functional programming and in programming languages in general.

Contact: Patrik Jansson + Joel Svensson (Mary Sheeran)

Number of people: 1-2