Name: Samuel Breese Description: Cryptography and Network Security - Toy DES implementation Language: Haskell Dependencies: - Recent release of GHC (tested on version 8.4.3) - bytestring library (https://hackage.haskell.org/package/bytestring) I wrote my implementation in Haskell. Perhaps more interesting is my use of relatively advanced type-level programming functionality in Haskell. Practically, this allows me to encode at least some correctness guarantees at the type level, ensuring that certain invariants are enforced at compile time. This is limited to bit string sizes here, but could be extended relatively easily to other constraints. This is clunkier than it would be in a language with real dependent types (which I am effectively faking here using DataKinds, GADTs, and TypeFamilies), and indeed I originally completed the assignment using Idris, but those languages often lack libraries for "real-world" functionality (e.g. networking, I/O in general, etc.). However, I hope this implementation can serve as both a submission for this assignment and a showcase of some basic and practical type-level verification techniques (formal verification and type systems are my area of research). To compile, it is probably easiest to use the Haskell Stack (https://docs.haskellstack.org/en/stable/README/). Once installed, it should be sufficient to simply enter this repository and run stack build --copy-bins --local-bin-path=. This will create a binary file called "crypto1", which can be given a command (either "encrypt" or "decrypt") and a key (as a ten-bit binary number) as command line arguments. It will then proceed to read from standard input and write to standard output until end-of-file. If you do not wish to use Stack, it should still be easy to compile and run. The only dependency from Hackage is the bytestring library, which is practically essential - I tried hard to avoid introducing any extraneous dependencies even if they would be useful, instead replicating the desired functionality internally (e.g., many functions from Control.Arrow). Networking is trivial by simply redirecting input and output streams to "netcat" from the shell. In the future, I might integrate networking natively, but as it stands it is more aesthetically pleasing to simply operate on streams and compose with other tools when additional functionality is required (per UNIX philosophy). Since this was explicitly stated to be acceptable on Piazza, I didn't worry about it too much. On another note: this implementation is not at all efficient, since bytes are treated as linked lists of booleans (using cons cells) that are destructed using pattern matching. The specified simple DES probably only needs 10-15 instructions per byte on modern architectures, where this implementation probably uses hundreds to thousands. If an efficient implementation using these formal method was desired, there are two approaches that come to mind: - deep embedding of a syntax for the operations, and then compilation - linear types Unfortunately, both of these approaches are unwarrantedly complex for an assigment. As such, I resign myself to a slow XOR implementation using 16 pattern matches instead of a single-instruction XOR on machine words.