• Stars
    star
    374
  • Rank 114,346 (Top 3 %)
  • Language
    Haskell
  • License
    BSD 3-Clause "New...
  • Created over 11 years ago
  • Updated almost 5 years ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

The Ivory EDSL

Build Status

Ivory

Ivory is an embedded domain specific language (EDSL) which aims to provide a systems-level programming language that removes some common pitfalls of programming in C, without sacrificing expressivity.

This repository includes a user guide and some examples Ivory programs. More information and tutorials are available on ivorylang.org.

The following paper describes the Ivory language:

  • Trevor Elliott, Lee Pike, Simon Winwood, Pat Hickey, James Bielman, Jamey Sharp, Eric Seidel, John Launchbury. Guilt-free Ivory. Haskell Symposium, 2015.

Please cite this paper for when citing the language.

Contents

  • ivory: the Ivory language implementation and interpreter
  • ivory-backend-c: a backend for compiling Ivory programs to C
  • ivory-examples: sample Ivory programs
  • ivory-opts: an optimization framework and some optimization implementations, for the Ivory AST.
  • ivory-bitdata: a macro language library for specifying bit-precise Ivory operations.
  • ivory-hw: a macro language library for writing hardware drivers in Ivory.
  • ivory-model-check: a backend for verifying Ivory programs with CVC4

Installing

Ivory is written in Haskell and uses several recent GHC extensions. It is known to work with with GHC 7.8.* and above.

We currently recommend using the Stack build tool for Ivory language packages and any programs which use them.

Copyright and license

Copyright 2013-2015 Galois, Inc.

Licensed under the BSD 3-Clause License; you may not use this work except in compliance with the License. A copy of the License is included in the LICENSE file.

Contributing

This project adheres to the Contributor Covenant code of conduct. By participating, you are expected to uphold this code. Please report unacceptable behavior to [email protected].

More Repositories

1

cryptol

Cryptol: The Language of Cryptography
Haskell
1,136
star
2

HaLVM

The Haskell Lightweight Virtual Machine (HaLVM): GHC running on Xen
Haskell
1,049
star
3

crucible

Crucible is a library for symbolic simulation of imperative programs
Rust
635
star
4

saw-script

The SAW scripting language.
Haskell
438
star
5

reopt

A tool for analyzing x86-64 binaries.
LLVM
284
star
6

haskell-tor

A Haskell implementation of the Tor protocol.
Haskell
267
star
7

swanky

A suite of rust libraries for secure multi-party computation
Rust
263
star
8

macaw

Open source binary analysis tools.
Haskell
195
star
9

MATE

MATE is a suite of tools for interactive program analysis with a focus on hunting for bugs in C and C++ code using Code Property Graphs.
Python
177
star
10

what4

Symbolic formula representation and solver interaction library
Haskell
148
star
11

cclyzerpp

cclyzer++ is a precise and scalable pointer analysis for LLVM code.
C++
133
star
12

HaNS

The haskell network stack
Haskell
113
star
13

dlkoopman

A general-purpose Python package for Koopman theory using deep learning.
Python
80
star
14

cereal

Haskell
77
star
15

ec2-unikernel

Tool for uploading unikernels into EC2
Haskell
77
star
16

smaccmpilot-build

An umbrella repository including all of the dependencies to build the smaccmpilot project
Makefile
72
star
17

daedalus

The Daedalus data description language
Haskell
66
star
18

blt

Lattice-based integer linear programming solver
C++
60
star
19

parameterized-utils

A set of utilities for using indexed types including containers, equality, and comparison.
Haskell
57
star
20

grift

Galois RISC-V ISA Formal Tools
Haskell
56
star
21

yapall

A precise and scalable pointer analysis for LLVM, written in Ascent
C
53
star
22

saw-core

The SAW core language.
Haskell
53
star
23

ddosflowgen

Simulate DDoS attacks and generate traffic datasets
Python
51
star
24

minlibc

C
49
star
25

llvm-pretty-bc-parser

Parser for the llvm bitcode format
LLVM
48
star
26

renovate

A library for binary analysis and rewriting
Haskell
47
star
27

FreeRTOS-Xen

FreeRTOS 7.6.0 ported to run as a Xen guest on ARM systems.
C
45
star
28

hacrypto

Experiments in high-assurance crypto.
C
43
star
29

lean4-balance-car

Lean4 port of Arduino balance car controller
C++
43
star
30

tower

A concurrency framework for the Ivory language
Haskell
41
star
31

lean-protocol-support

This project contains various supporting libraries for lean to reason about protocols.
Lean
38
star
32

jvm-parser

A Haskell parser for JVM bytecode files
Haskell
37
star
33

flexdis86

A library for disassembling x86-64 binaries.
Haskell
36
star
34

halfs

The Haskell File System: A file system implementation in Haskell
Haskell
36
star
35

elf-edit

The elf-edit library provides a datatype suitable for reading and writing Elf files.
Haskell
35
star
36

semmc

Stratified synthesis for learning machine code instruction semantics
Haskell
35
star
37

mir-verifier

SAW front end for the MIR language from rustc
HTML
34
star
38

fancy-garbling

Rust implementation of the BMR16 arithmetic garbling scheme.
Rust
33
star
39

smaccmpilot-stm32f4

SMACCMPilot flight controller
JavaScript
32
star
40

pure-zlib

A Haskell-only implementation of zlib / DEFLATE.
Haskell
31
star
41

helib-demos

Experiments in homomorphic encryption
C++
30
star
42

FiveUI

Extensible UI Analysis in your browser
JavaScript
29
star
43

lean-llvm

LLVM support for the lean theorem prover
Lean
28
star
44

llvm-pretty

An llvm pretty printer inspired by the haskell llvm binding
Haskell
28
star
45

galua

Lua debugger and interpreter
JavaScript
27
star
46

BESSPIN

Top-level repository including all relevant BESSPIN repository
26
star
47

curl

A Haskell binding to the curl library
Haskell
26
star
48

json

Haskell JSON library
Haskell
25
star
49

estimator

State-space estimation algorithms and models
Haskell
25
star
50

dismantle

A library of assemblers and disassemblers derived from LLVM TableGen data
HTML
25
star
51

xml

Haskell XML library
Haskell
25
star
52

http-server

A Haskell HTTP server
Haskell
23
star
53

llvm-verifier

The LLVM Symbolic Simulator, part of SAW.
Haskell
21
star
54

RSA

Haskell RSA Library
Haskell
20
star
55

msf-haskell

Haskell implementation of Metasploit remote API
Haskell
20
star
56

FAW

Galois Format Analysis Workbench
HTML
20
star
57

cryfsm

convert simple cryptol expressions into finite-state machines
Haskell
20
star
58

BLST-Verification

BLST-Verification
Python
20
star
59

lean-haskell-bindings

Haskell Bindings to the Lean Theorem Prover http://leanprover.github.io/
Haskell
19
star
60

sqlite

A simple sqlite3 library for Haskell
C
19
star
61

cryptol-specs

A central repository for specifications of cryptographic algorithms in Cryptol
TeX
18
star
62

surveyor

A symbolic debugger for C/C++ (via LLVM), machine code, and JVM programs
Haskell
18
star
63

mistral

An interpreter for the Mistral language.
Haskell
18
star
64

LinearArbitrary-SeaHorn

LinearArbitrary-SeaHorn is a CHC solver for LLVM-based languages.
C
17
star
65

HARDENS

Repository for the HARDENS project
Jupyter Notebook
17
star
66

scuttlebutt

Multi-party computation utilities toolkit for rust
Rust
16
star
67

cryptol-semantics

Semantics for Cryptol
Coq
16
star
68

e2eviv

Artifacts associated with the U.S. Vote Foundation's E2E-VIV Project (end-to-end verifiable internet voting).
TeX
16
star
69

pate

Patches Assured up to Trace Equivalence
Haskell
15
star
70

halvm-web

Haskell
15
star
71

pads-haskell

A domain specific language for processing ad-hoc data.
Haskell
14
star
72

ardupilot-mega

Fork: DO NOT SUBMIT PULL REQS/BUG REPORTS HERE
C
14
star
73

reopt-vcg

A translation verifier for Reopt (https://github.com/GaloisInc/reopt)
SMT
14
star
74

sat2015-crypto

Slides and examples to accompany the September 25th invited talk at SAT 2015
TeX
14
star
75

ICryptol

IPython-style interaction for Cryptol
Haskell
14
star
76

ivory-tower-stm32

Tower backend and Ivory board support package for the STM32 line of microcontrollers
C
12
star
77

AMIDOL

Scientific model creation toolset.
HTML
12
star
78

hpb

Haskell Protocol Buffers
Haskell
12
star
79

golang

Parser and type analysis for the Go programming language
Haskell
12
star
80

mime

A Haskell MIME library
Haskell
12
star
81

LIMA

LIMA: Language for Integrated Modeling and Analysis
Haskell
12
star
82

gec

Embedded-friendly crypto a la SMACCM
Haskell
12
star
83

SHA

Haskell implementation of SHA / SHA2 hash functions
Haskell
12
star
84

alex-tools

A Haskell library making it easier to write Alex lexers.
Haskell
12
star
85

nasa-affirm

Architectural Framework For Integrated Refinement Modeling
HTML
11
star
86

regex-fsm

Convert regular expressions into efficient matrix branching programs
Haskell
11
star
87

salty

A DSL for generating GR(1) problems
JavaScript
11
star
88

simple-tar

A very simple tar archive processing library
Haskell
11
star
89

ocelot

Oblivious transfer library for rust
Rust
11
star
90

csaf

Control Systems Analysis Framework - a framework to minimize the effort required to evaluate, implement, and verify controller design (classical and learning enabled) with respect to the system dynamics.
Python
11
star
91

hexdump

A human readable style for binary data.
Haskell
11
star
92

gidl

Gidl: an Interface Description Language
Haskell
11
star
93

saw-core-coq

A translator from SAWCore to Coq
Coq
11
star
94

BESSPIN-Voting-System-Demonstrator-2019

The BESSPIN Voting System. This system is used to demonstrate and red team SSITH secure CPUs.
Coq
11
star
95

argo

A Haskell library for building JSON-RPC servers (work in progress), with servers for Cryptol and SAW
Haskell
11
star
96

lustre

A parser and AST for Lustre
Haskell
11
star
97

rustwall

Rust firewall for seL4
Rust
10
star
98

arm-asl-parser

Parsing tools for ARM's ASL
Java
10
star
99

ivory-rtverification

Runtime verification for C code via a GCC plugin architecture.
Haskell
10
star
100

cryptol-verifier

The Cryptol Symbolic Simulator, part of SAW.
Haskell
9
star