April | 2009 | Ulisses Costa Blog

Anamorphisms in Haskell

8 04 2009

First I would like to introduce the notation that I use here. The pointfree notation is good to see a program (functions) data flow and as composition of functions, combination of functions, if you prefer. This style is characterized by not using variables in declaration of functions. Haskell allow us to implement that notation natively. The dual of the pointfree notation is the pointwise one.

A simple example of a function in pointwise style:

f n = (n+2)*10 -- pointwise

The dual in pointfree would be:

f = (*10) . (+2) -- pointfree

Clarifications

First of all to define a function, for example $f$ , i can say:

$\xymatrix {\mathbb{N} \ar[r]^{f} & \mathbb{R}}$ , $\xymatrix {\mathbb{R} & \mathbb{N}\ar[l]^{f}}$ or $\xymatrix {\mathbb{N} \ar[d]^{f} \\ \mathbb{R}}$ .

I will assume that you are familiarized with infix notation, $either$ , and composition $(\circ)$ functions.

Types

For this post I need to explain the data type we will going to use. In Haskell we define it by:

data Tree a = Node a [Tree a]

Let’s create the same, but more convenient. Consider the following isomorphic type for $Tree$ :

data Tree a = Node (a, [Tree a])

We could see $Node$ as a the following function:

Node :: (a, [Tree a]) -> Tree a

So typologically we have $(a, [Tree~a])$ . We use $(\times)$ to define that two things occurs in parallel, like tuples do, so we can redefine it: $(a \times~[Tree~a])$

Now we can say that $(Tree~a)$ is isomorphic to $(a \times~[Tree~a])$ .
This is something to say that $(Tree~a)$ and $(a \times~[Tree~a])$ keep the same information without any change. We represent that formally as: $(Tree~a) \cong~(a \times~[Tree~a])$ .

Anamorphisms

Let $A$ , $B$ , $C$ , $D$ be Inductive data types (sets) and $in$ , $ana$ , $rec$ functions.

$\xymatrix@!=10pc{A \ar[r]^{h} \ar[d]^{ana(h)_{Tree}} & B \ar[d]^{rec_{Tree}} \\C & D\ar[l]^{in_{Tree}}\\}$

$ana(h_{Tree})$ is the anamorphism of $h$ if the diagram commute.

We use the notation $rec_{Tree}$ to say that function $rec$ in not generic, but only works for data $Tree$ . The same happens with $in$ and $ana$ . We will write $ana(h)_{Tree}$ using the composition of $in$ , $ana$ and $rec$ functions. That way we are breaking our problem in small ones. So, in the end we will have the following definition for $ana(h)_{Tree}$ :

$ana(h)_{Tree} = in_{Tree} \circ rec_{Tree} \circ h$

The function that we want is $ana(h)$ , and that function is over $(Tree~a)$ so we have:

ana :: (A -> B) -> A -> Tree c

Type $C$ is $(Tree~c)$ . Maybe this isn’t clear yet, let’s start with function $in$

function in

The function $in_{Tree}$ is responsible to create the isomorphism between $(Tree~a)$ and $(a \times~[Tree~a])$ , so the code could be something like this:

inTree :: Tree a -> (a, [Tree a])
inTree    = Node

In Haskell we represent the type $(\times)$ as $(,)$ . So, type $D$ is $(a \times~[Tree~a])$ . So by now, we already know the following unifications $C \sim Tree~c$ and $D \sim c \times~[Tree~c]$ . So now our graphic is:
$\xymatrix@!=10pc{A \ar[r]^{h} \ar[d]^{ana(h)_{Tree}} & B \ar[d]^{rec_{Tree}} \\Tree~c & c \times~[Tree~c]\ar[l]^{in_{Tree}}\\}$

function $h$

The function $h$ is also known as *gen*, here is where we said the step that pattern do. This is the only function we need to take care, if this function is good, our problem is solved. Now image that our problem is:

Suppose that the pair of positive integers (v, p) denotes the number of red balls (v) and black (p) that is inside a bag, the balls which are taking randomly, successively, until the bag is empty.

This is the point-wise version of the function we want to convert to pointfree using anamorphisms. This function represent as a tree, all possible states of the bag over these experiences.

state :: (Int,Int) -> Tree (Int,Int)
state(0,0) = Node (0,0) []
state(v,0) = Node (v,0) [state(v-1,0)]
state(0,p) = Node (0,p) [state(0,p-1)]
state(v,p) = Node (v,p) [state(v-1,p),state(v,p-1)]

If we want that “latex state$ became an anamorphism, we have to say that our type $A$ unify ( $\sim$ ) with $Int \times~Int$ , and $Tree~c$ became more restrict, and unify with $Tree (Int \times~Int)$ . A consequence of changing the co-domain of $in_{Tree}$ is changing the domain of it to $(Int \times~Int) \times~[Tree (Int \times~Int)]$ . We represent $ana(h)$ as $[( h )]$ . Now we can be more specific with our graphic:

$\xymatrix@!=14pc{Int \times~Int \ar[r]^{h} \ar[d]^{[(h)]_{Tree}} & B \ar[d]^{rec_{Tree}} \\Tree~(Int \times~Int) & (Int \times~Int) \times~[Tree~(Int \times~Int)]\ar[l]^{in_{Tree}}\\}$

function rec

Here we have to get a function $rec$ that co-domain is $(Int \times~Int) \times~[Tree~(Int \times~Int)]$ . Probably the best is to pass the first part of the tuple (part with type $(Int \times~Int)$ ) and the rest (part with type $[Tree~(Int \times~Int)]$ ) is just a $map$ of the function $[(h)]_{Tree}$ . So, now our graphic is:

$\xymatrix@!=14pc{Int \times~Int \ar[r]^{h} \ar[d]^{[(h)]_{Tree}} & (Int \times~Int) \times~[(Int \times~Int)] \ar[d]^{rec_{Tree}} \\Tree~(Int \times~Int) & (Int \times~Int) \times~[Tree~(Int \times~Int)]\ar[l]^{in_{Tree}}\\}$

As you can see, the second part of the co-domain of $h$ is the type of function $map~[(h)]_{Tree}$ :

$map~[(h)]_{Tree}~:~[(Int \times~Int)] \rightarrow~[Tree(Int \times~Int)]$

So our final graphic became:

$\xymatrix@!=14pc{Int \times~Int \ar[r]^{h} \ar[d]^{[(h)]_{Tree}} & (Int \times~Int) \times~[(Int \times~Int)] \ar[d]^{id \times~map~[(h)]_{Tree}} \\Tree~(Int \times~Int) & (Int \times~Int) \times~[Tree~(Int \times~Int)]\ar[l]^{in_{Tree}}\\}$

Now, we just have to define the function $h$ and apply them to our anamorphism of $Tree$ .

h :: (Int, Int) -> ( (Int, Int), [ (Int, Int) ] )
h(0,0) = ( (0,0), [] )
h(v,0) = ( (v,0), [ (v-1,0) ] )
h(0,p) = ( (0,p) [ (0,p-1) ] )
h(v,p) = ( (v,p), [ (v-1,p), (v,p-1) ] )

And this is it! Now we can say that:
$state \equiv~ana_{Tree}$ where $ana(h)_{Tree} = in_{Tree} \circ~id~><~map~ana(h)_{Tree} \circ h$

Outroduction

Here is all the code you need to run this example in Haskell:

module AnamorphismExample where

infix 5 ><

i1 = Left
i2 = Right
p1 = fst
p2 = snd

data Tree a = Node (a, [Tree a]) deriving Show

split :: (a -> b) -> (a -> c) -> a -> (b,c)
split f g x = (f x, g x)

(><) :: (a -> b) -> (c -> d) -> (a,c) -> (b,d)
f >< g = split (f . p1) (g . p2)

inTree :: (a, [Tree a]) -> Tree a
inTree = Node

anaTree h = inTree . (id >< map (anaTree h)) . h

-- our function
h_gen :: (Int, Int) -> ( (Int, Int), [ (Int, Int) ] )
h_gen(0,0) = ( (0,0), [] )
h_gen(v,0) = ( (v,0), [ (v-1,0) ] )
h_gen(0,p) = ( (0,p) , [ (0,p-1) ] )
h_gen(v,p) = ( (v,p), [ (v-1,p), (v,p-1) ] )

state = anaTree h_gen

Pass a year since I promised this post. The next will be on hylomorphisms I promise not take too that much.

Comments : 6 Comments »
Tags: anamorphism, code, English, functions, haskell, mathematics, mp1, pointfree, programming, recursion, Theoretical fundations
Categories : Uncategorized

Capture and dissect network traffic

1 04 2009

Currently I am doing research at the University of Minho in the group of distributed systems, with duration of one year. My job is to find a way to identify specific links between a user and a distributed system. The general idea is to draw a map of services in a distributed system. This post only refers to the first milestone.

The proposal was to make such a system using Snort.

Snort

Snort is a Network intrusion detection system, that means with Snort you can detect malicious activity in your network. We can detect many types of network attacks. We can identify DoS, DDoS attacks, port scans, cracking attempts, and much more.

Snort can operate in two different ways. We can set up Snort to run in passive mode, putting it to listen in promiscuous mode. That is, because Ethernet network switches send traffic to all computers connected to itself, we get traffic addressed to other machines on the network. To do this we only need to connect to the network and turn Snort on in our machine, no one knows that we are recording every traffic (including traffic destined for other computers).

Snort may also run in active mode. This “active” is not able to modify the data channel, but to be able to be installed in a network, a router for example and reap more information than in passive mode. Thus it makes sense to use the capacity of rules that Snort supports, to filter the traffic that it read.

To do this, Snort capture all packets that pass the network and interprets each. As the rules we have defined Snort tries to find these patterns in each packet, or each set of packets and take certain actions for each of them.

For example, if a large number of TCP requests reach a particular host, to a large number of ports in a short space of time we probably are the target of a port scan. NIDS like Snort know how to find these patterns and alerting the network administrator.

Objective

Our aim was to use Snort to capture all traffic into passive mode.

root@pig:# snort -u snort -g snort -D -d -l /var/log/snort -c /etcsnort/snort.debian.conf -i eth0

We are saving the logs in binary (tcpdump format), for that I use the “-d -l /dir/” flags. I prefer to save all the packets into binary because is more easier to parse, than the structure of files and directories that Snort creates by default.

I started by trying to use some language that advised me to try to do the parsing of the file created by snort. Initially started to use python, but only find a tcpdump parser and could not get more than one file translated in tcpdump to hexadecimal.
After that I tried to use Haskell and I was amazed!

Haskell and packet parsing

House is a Haskell Operative System done by The Programatica Project.

This is a system than can serve as a platform for exploring various ideas relating to low-level and system-level programming in a high-level functional language.

And indeed helped me a lot in doing my job. This project have already done a lot of parsers for network packets. It implements the Ethernet, IPv4, IPv6, TCP, UDP, ICMP, ARP and I think is all.

The libpcap (tcpdump parser) is already implemented in Haskell too, so is very simple to parse a complete packet:

getPacket :: [Word8] -> InPacket
getPacket bytes =  toInPack $ listArray (0,Prelude.length bytes-1) $ bytes

-- Ethernet | IP | TCP | X
getPacketTCP :: [Word8] -> Maybe (NE.Packet (NI4.Packet (NT.Packet InPacket)))
getPacketTCP bytes = doParse $ getPacket bytes :: Maybe (NE.Packet (NI4.Packet (NT.Packet InPacket)))

As you can see is too easy to have a compete structure of a packet parsed with this libraries. The problem is that they don’t have already implemented a application packet parser. So, according to that image:

This is the level of depth we can go with this libraries. What is very good, but not perfect for me :S

My supervisor told me to start searching a new tool to do this job. I was sad because I could not do everything in Haskell. But it is already promised that I will continue this project in Haskell. You can see the git repo here.

I find tshark, a great tool to dissect and analyze data inside tcpdump files.

The power of tshark

tshark is the terminal based Wireshark, with it we can do everything we do with wireshark.

Show all communications with the IP 192.168.74.242

root@pig:# tshark -R "ip.addr == 192.168.74.242" -r snort.log

...
7750 6079.816123 193.136.19.96 -> 192.168.74.242 SSHv2 Client: Key Exchange Init
7751 6079.816151 192.168.74.242 -> 193.136.19.96 TCP ssh > 51919 [ACK] Seq=37 Ack=825 Win=7424 Len=0 TSV=131877388 TSER=1789588
7752 6079.816528 192.168.74.242 -> 193.136.19.96 SSHv2 Server: Key Exchange Init
7753 6079.817450 193.136.19.96 -> 192.168.74.242 TCP 51919 > ssh [ACK] Seq=825 Ack=741 Win=7264 Len=0 TSV=1789588 TSER=131877389
7754 6079.817649 193.136.19.96 -> 192.168.74.242 SSHv2 Client: Diffie-Hellman GEX Request
7755 6079.820784 192.168.74.242 -> 193.136.19.96 SSHv2 Server: Diffie-Hellman Key Exchange Reply
7756 6079.829495 193.136.19.96 -> 192.168.74.242 SSHv2 Client: Diffie-Hellman GEX Init
7757 6079.857490 192.168.74.242 -> 193.136.19.96 SSHv2 Server: Diffie-Hellman GEX Reply
7758 6079.884000 193.136.19.96 -> 192.168.74.242 SSHv2 Client: New Keys
7759 6079.922576 192.168.74.242 -> 193.136.19.96 TCP ssh > 51919 [ACK] Seq=1613 Ack=1009 Win=8960 Len=0 TSV=131877415 TSER=1789605
...

Show with a triple: (time, code http, http content size), separated by ‘,’ and between quotation marks.

root@pig:# tshark -r snort.log -R http.response -T fields -E header=y -E separator=',' -E quote=d -e frame.time_relative -e http.response.code -e http.content_length

...
"128.341166000","200","165504"
"128.580181000","200","75332"
"128.711618000","200","1202"
"149.575548000","206","1"
"149.719938000","304",
"149.882290000","404","338"
"150.026474000","404","341"
"150.026686000","404","342"
"150.170295000","304",
"150.313576000","304",
"150.456650000","304",
...

Show a tuple of arity 4 with: (time, source ip, destination ip, tcp packet size).

root@pig:# tshark -r snort.log -R "tcp.len>0" -T fields -e frame.time_relative -e ip.src -e ip.dst -e tcp.len

...
551.751252000   193.136.19.96   192.168.74.242  48
551.751377000   192.168.74.242  193.136.19.96   144
551.961545000   193.136.19.96   192.168.74.242  48
551.961715000   192.168.74.242  193.136.19.96   208
552.682260000   193.136.19.96   192.168.74.242  48
552.683955000   192.168.74.242  193.136.19.96   1448
552.683961000   192.168.74.242  193.136.19.96   1448
552.683967000   192.168.74.242  193.136.19.96   512
555.156301000   193.136.19.96   192.168.74.242  48
555.158474000   192.168.74.242  193.136.19.96   1448
555.158481000   192.168.74.242  193.136.19.96   1400
556.021205000   193.136.19.96   192.168.74.242  48
556.021405000   192.168.74.242  193.136.19.96   160
558.874202000   193.136.19.96   192.168.74.242  48
558.876027000   192.168.74.242  193.136.19.96   1448
...

Show with a triple: (source ip, destination ip, port of destination ip).

root@pig:# tshark -r snort.log -Tfields  -e ip.src -e ip.dst -e tcp.dstport

...
192.168.74.242  193.136.19.96   37602
192.168.74.242  193.136.19.96   37602
193.136.19.96   192.168.74.242  22
192.168.74.242  193.136.19.96   37602
193.136.19.96   192.168.74.242  22
193.136.19.96   192.168.74.242  22
192.168.74.242  193.136.19.96   37602
192.168.74.242  193.136.19.96   37602
192.168.74.242  193.136.19.96   37602
193.136.19.96   192.168.74.242  22
193.136.19.96   192.168.74.242  22
193.136.19.96   192.168.74.242  22
193.136.19.96   192.168.74.242  22
192.168.74.242  193.136.19.96   37602
192.168.74.242  193.136.19.96   37602
...

Statistics

Hierarchy of protocols

root@pig:# tshark -r snort.log -q -z io,phs

frame                                    frames:7780 bytes:1111485
  eth                                    frames:7780 bytes:1111485
    ip                                   frames:3992 bytes:848025
      tcp                                frames:3908 bytes:830990
        ssh                              frames:2153 bytes:456686
        http                             frames:55 bytes:19029
          http                           frames:5 bytes:3559
            http                         frames:3 bytes:2781
              http                       frames:2 bytes:2234
                http                     frames:2 bytes:2234
          data-text-lines                frames:10 bytes:5356
        tcp.segments                     frames:3 bytes:1117
          http                           frames:3 bytes:1117
            media                        frames:3 bytes:1117
      udp                                frames:84 bytes:17035
        nbdgm                            frames:50 bytes:12525
          smb                            frames:50 bytes:12525
            mailslot                     frames:50 bytes:12525
              browser                    frames:50 bytes:12525
        dns                              frames:34 bytes:4510
    llc                                  frames:3142 bytes:224934
      stp                                frames:3040 bytes:182400
      cdp                                frames:102 bytes:42534
    loop                                 frames:608 bytes:36480
      data                               frames:608 bytes:36480
    arp                                  frames:38 bytes:2046

Conversations

We use: -z conv,TYPE,FILTER

TYPE could be:

eth,
tr,
fc,
fddi,
ip,
ipx,
tcp,
udp

And the filters are used to restrict the statistics.

root@pig:# tshark -r snort.log -q -z conv,ip,tcp.port==80

================================================================================
IPv4 Conversations
Filter:tcp.port==80
                                |           | |    Total    |
                                |Frames Bytes | |Frames Bytes | |Frames Bytes |
193.136.19.148  192.168.74.242 141    13091    202   259651    343   272742
192.168.74.242  128.31.0.36     22     6858     28     4784     50    11642
================================================================================

IO

We use: -z io,stat,INT,FILTER,…,FILTER

root@pig:# tshark -r snort.log -q -z io,stat,300,'not (tcp.port=22)'

===================================================================
IO Statistics
Interval: 300.000 secs
Column #0:
                |   Column #0
Time            |frames|  bytes
000.000-300.000    2161    543979
300.000-600.000    1671    264877
600.000-900.000     508     46224
900.000-1200.000     185     12885
1200.000-1500.000     201     14607
1500.000-1800.000     187     13386
1800.000-2100.000     189     13887
2100.000-2400.000     187     13386
2400.000-2700.000     189     13887
2700.000-3000.000     187     13386
3000.000-3300.000     185     12885
3300.000-3600.000     189     13887
3600.000-3900.000     210     15546
3900.000-4200.000     189     13887
4200.000-4500.000     187     13386
4500.000-4800.000     185     12885
4800.000-5100.000     189     13887
===================================================================

Conclusion

With tshark we could do everything we want to know what is inside a network packet. The trick is to understand the statistics that tshark generate, and know how to ask it.

Now my work will get a machine to run Snort in an active mode and begin to understand how to use Snort to do all this work of collecting information.

If you feel interested and understand Portuguese, see the presentation:

Comments : 1 Comment »
Tags: code, English, hacking, haskell, house, http, internet, libpcap, linux, network, programming, research, scanners, security, snort, software, statistics, tcpdump, uminho, unix, xml
Categories : Uncategorized

Cryptol the language of cryptography

1 04 2009

Pedro Pereira and I are working on a new project in the Masters. The second half of the Masters is composed of a single project suggested by a company. Some companies are forming partnerships in the Masters formal methods, including: the Critical software, SIG and Galois. We chose the Galois because we also are in the area of cryptography and we already knew some work of some people from this company.

The project suggested by Galois was study the Cryptol as a language of specification of cryptographic algorithms. The cipher we used for this study is the SNOW 3G (The SNOW website), later on I will talk about the specification of this cipher. In this post I am only interested to show the language.

I’m going to show you some details about the language. This post is not intend to be a exhaustive explanation of Cryptol, if you looking for that you can go directly to the manuals. This post only relates my experience, and what I like it most with the language.

Overview

Cryptol is a high-level language that is geared to deal with low-level problems. Is a Domain-specific language to design and implement cryptographic algorithms.
This language has a high percentage of correctness of the implementation of a cipher, because it implements type inference, so we can say that a big part of the language implements correctness. This correctness is also achieved thanks to the architecture of the language – functional. We don’t have side effects – a function only return something inside is codomain.
In Cryptol we have this philosophy that says that everything is a sequence. This is very useful because we are working with low level data (array of bits), so we use sequences to represent that arrays. We can have nested sequences to have a more structured representation of data. For example, we can simply transform a 32-bit sequence in a 4 1-byte sequence.
The size of this sequences could be implemented as finite or infinite, as we going to see later in this post. Because Cryptol is a high-level language we can also implement polymorphic functions, most of the primitive functions are implemented in polymorphic mode. The way we have to navigate throw the sequences is using recursion, or sequences comprehension, and with these two techniques we can implement recurrences.

If you are a Haskell programmer you just need the next section to learn Cryptol. This language is so look a like with Haskell that even the philosophy seems to have a lot in commune.

Types in Cryptol

The type $[32]$ means that you have a sequence of 32-bit size. All the types in Cryptol are size oriented. The unit is the $Bit$ , that you can use to represent $Bool$ . To represent a infinite sequence we use the reserved word $inf$ , and we write: $[inf]$ to represent that.

If you want to generate a infinite sequence, we use the syntactic sugar of the sequences like that: $[1~..]$ . Cryptol will infer this sequence as type

$[1~..]~:~[inf][1]$

That means this sequence have infinite positions of 1-bit words. The type inference mechanism will always optimize the size that he needs, to represent the information.
So, it infer the type of $[100~..]$ as:

$[100~..]~:~[inf][7]$

Because, it “knows” that needs only 7-bits to represent the decimal $100$ . But if you need more, you can force the type of your function.
We implement polymorphism in our types, if we have:

$f~:~[a]b~\rightarrow~[a]b$

This means, that the function $f$ have polymorphism over $b$ , because we say that it domain is one sequence of size $a$ of type $b$ , and it codomain also. Here we could also see: $f~:~[a][b]c$ meaning that $f$ is a constant of sequences of size $b$ of type $c$ , $a$ times.

So, lets talk about some primitive functions in Cryptol, and its types. The $tail$ function have the following type in Cryptol:

$tail~:~\{a~b\}~[a+1]b~\rightarrow~[a]b$

As we can see, Cryptol is so size oriented, that we can use arithmetic operators in types. We can probably infer what this function does just from it type: $tail$ works for all $a$ and $b$ such that if we have one sequence os size $a+1$ of type $b$ it returns one sequence of size $a$ of same type. In fact this function removes the first element of one sequence.

Because of this size oriented philosophy a lot of functions, that change the size of the sequences can be read just from the type.

As you can see in the following list of Cryptol primitive function:

$drop~:~\{ a~b~c \}~( fin~a ,~a~\geq~0)~\Rightarrow~(a ,[ a + b ]~c )~\rightarrow~[ b ]~c$
$take~:~\{ a~b~c \}~( fin~a ,~b~\geq~0)~\Rightarrow~(a ,[ a + b ]~c )~\rightarrow~[ a ]~c$
$join~:~\{ a~b~c \}~[ a ][ b ] c~\rightarrow~[ a * b ]~c$
$split~:~\{ a~b~c \}~[ a * b ] c~\rightarrow~[ a ][ b ]~c$
$tail~:~\{ a~b \}~[ a +1] b~\rightarrow~[ a ]~b$

Recursion and Recurrence

Cryptol implements Recursion, just like a lot of functional languages do.

Imagine the fibonacci function definition:

It implementation in Crytol is exactly the same as defined mathematically.

fib : [inf]32 -> [inf]32;
fib n = if n == 0 then 0 else if n == 1 then 1 else fib (n-1) + fib (n-2);

Cryptol uses recursion to permit us to iterate throw sequences.

But, If you prefer you can implement a more functional algorithm of fibonacci function in Cryptol:

fib : [inf]32 -> [inf]32;
fib n = fibs @ n;
   where {
      fibs : [inf]32;
      fibs = [0 1] # [| x + y || x <- drop (1,fibs) || y <- fibs |];
   };

Here, as you can see, we define a infinite list $fibs$ of all the fibonacci numbers, by calling the $fibs$ inside the sequences comprehension $fibs$ , this is called a recurrence, and you can use that too in Cryptol.

Cryptol vs C

I’m going to show you some part of the implementation of SNOW 3G in C. This is a function called $MUL_{\alpha}$

MULa : [8] -> [32];
MULa(c) = join ( reverse [
   ( MULxPOW(c, 23 :[32], 0xA9) )
   ( MULxPOW(c, 245:[32], 0xA9) )
   ( MULxPOW(c, 48 :[32], 0xA9) )
   ( MULxPOW(c, 239:[32], 0xA9) ) ] );

/* The function MUL alpha.
    Input c: 8-bit input.
    Output : 32-bit output.
    See section 3.4.2 for details.
 \*/
u32 MULalpha(u8 c) {
 return
  ((((u32)MULxPOW(c,23, 0xa9)) << 24 ) |
  (((u32)MULxPOW(c, 245,0xa9)) << 16 ) |
  (((u32)MULxPOW(c, 48,0xa9)) << 8 ) |
  (((u32)MULxPOW(c, 239,0xa9)))) ;
}

You can see that in Cryptol we just say that we want to work with a 32-bit word, and we don’t need to do any shift to our parts of the word. We just join them together. We reverse the sequence, because Cryptol stores words in little-endian, and we want to keep the definition like the specification.

This is a very simple function, so the result in C is not so that different. But if we have a more complex function, we were going to start having a nightmare to write that in C.

Conclusion

Well, the conclusion is that Cryptol is a language that really help to write low-level algorithms. With Cryptol the specification is formal and easier to read than other languages. A value of Cryptol is that the code can be converted to other languages, such as VHDL and C.

If you’re interested, take a look at the presentation that we did.

References

Comments : Leave a Comment »
Tags: cipher, code, comprehension list, cryptography, Cryptol, English, functions, haskell, internet, language, linux, mathematics, msc, programming, recursion, research, security, software, types, uminho
Categories : Uncategorized

Ulisses Costa Blog

Anamorphisms in Haskell

Clarifications

Types

Anamorphisms

function in

function $h$

function rec

Outroduction

Capture and dissect network traffic

Snort

Objective

Haskell and packet parsing

The power of tshark

Statistics

Conversations

IO

Conclusion

Cryptol the language of cryptography

Overview

Types in Cryptol

Recursion and Recurrence

Cryptol vs C

Conclusion

References

Feed

Books

Archive

Recent Posts

Blogroll

Favorite Sites

Friends

Tags

del.icio.us

Planet Haskell

Follow “Ulisses Costa Blog”