LiquidHaskell at Awake Networks
























Verification of Packet Analysis


Jenkis (used to) run liquid on all but 4 files

Files known to fails

  • Data.Struct.[Checked/Unchecked]: John's dependent types magic
  • Awake/Data/[Chunks/Buffer]: Deep list invariants (known but time consuming)























Experience


Bug examples


Annotations in Numbers


Annotations are 2.34% of the code!

                                   LOC   LLOC Termination+ Assumes Pragma


Total (74 files)                  20984   491   28(40)-13    19    41 (case,trust,prune,scrape,linear)

+Termination = annotated functions (loc for annotations) - lazy functions

                                   LOC   LLOC Termination+ Assumes Pragma


│── Awake                           
│   │   Data
│   │   ├── AppConfig.hs             24   0    0             0       0       
│   │   ├── Bounds.hs                42   0    0             0       0  
│   │   ├── Buffer.hs               423   1    1(1)          0       0
│   │   ├── Chunks.hs               100   0    0             0       0 
│   │   ├── Endian.hs               123   0    0             0       0 
│   │   ├── Extract.hs              305   0    0             0       0   
│   │   ├── Forgettable.hs          137   1    0             0     1 (prune) 
│   │   ├── Internalizeable.hs      14    0    0             0       0 
│   │   ├── Maybe
│   │   │   └── Type.hs             55    0    0             0       0 
│   │   ├── Packet
│   │   │   ├── DPDK.hs             337   4    1(2)          0       0          
│   │   │   ├── Linux.hs            323   4    2(2)          0     1 (scrape)
│   │   │   └── PCAP.hs             219   3    1             1     1 (scrape)
│   │   ├── Packet.hs                23   0    0             0       0          
│   │   ├── Sessions.hs             125   0    0             0       0 
│   │   ├── Struct
│   │   │   ├── Checked.hs          155   7    0             0       0 
│   │   │   ├── Examples.hs          51   0    0             0       0   
│   │   │   └── Unchecked.hs        465   8    0             0       0 
│   │   └── Struct.hs               258   4    0             1       0   
│   ├── Fused.hs                    674   3    0             0     1 (prune)
│   ├── Generator.hs               1014  18    3(5)-1        1     1 (prune)
│   ├── Parser
│   │   └── Multiplier.hs           172  21    0             1+    1 (prune)
│   ├── Protocol
│   │   ├── ASN1.hs                1024  16    3(3)-1        0     2 (case,trust)          
│   │   ├── DNS.hs                  285   2    0             0     2 (case,trust)          
│   │   ├── Ethernet.hs             168   5    0             0     1 (trust)
│   │   ├── FTP.hs                  536   0    0             0       0                          
│   │   ├── HTTP.hs                 835  24*   2(2)-3        2     4 (case,trust,prune,scrape)
│   │   ├── ICMP.hs                 384   6    0             2     2 (case,trust)
│   │   ├── IP.hs                   477  14    0             2     2 (case,trust) 
│   │   ├── IPv4.hs                 174   7    0             0     2 (case,trust) 
│   │   ├── IPv6.hs                 120   7    0             0     2 (case,trust)    
│   │   ├── Kerberos.hs             872   2    0             0     2 (case,trust)         
│   │   ├── LDAP.hs                 909   3    0             0     3 (case,trust,prune) 
│   │   ├── NTLM.hs                 328   0    0             0        0
│   │   ├── SMB.hs                 1531   4    1(1)          0     2 (case,trust)
│   │   ├── SPNEGO.hs               117   0    0             0        0 
│   │   ├── TCP.hs                 1349   9    0             0     3 (case,trust,prune)
│   │   ├── TFTP.hs                 548   5    0             0        0 
│   │   ├── TLS.hs                  685  10    1(1)          0        0 
│   │   └── UDP.hs                  270   1    0             1        0 
│   ├── Protocol.hs                  38   0    0             0        0 
│   ├── ProtocolBuffers (19 fs)    1914   0    0             0        0          
│   ├── ProtocolBuffers.hs            9   0    0             0        0            
│   ├── Streaming.hs                250   2                  0     2 (case,trust)
│   ├── System
│   │   └── Testimony.hs            564   7    0-1           2**   1 (prune) 
│   ├── Text             (2 fs)     103   0    0             0        0  
│   └── Util.hs                     347   6    4(5)-1        0        0
├── Data
│   ├── ByteString
│   │   ├── Extras.hs               610 179    2(10)         6        0 
│   │   └── Parser.hs                86   0    0             0        0 
│   ├── ListOr.hs                   139   1    0             0     1 (trust)
│   ├── Map
│   │   └── Lazy
│   │       └── Extras.hs            26   0    0             0        0  
│   ├── Monoid
│   │   └── Extras.hs               549  43   1(1)           0     2 (linear,scrape)
│   └── StrictPair.hs                22   0    0             0        0  
├── Network
│   └── Kafka
│       └── Extras.hs                45   0    0             0        0  
├── Parser
    └── Bidirectional.hs            631  64   7(7)-6         0     2 (trust,prune)



* 20 lines of measures, ghc complained for unsued 

Note: reasons for assumes 
  - dependent type invariants 
  - constants (bytestring length)
  - import functions 























LiquidHaskell at Awake Networks
























Thank You!



cabal install liquidhaskell
http://www.refinement-types.org
online demo @ http://goto.ucsd.edu/liquidhaskell