Explore @GaloisInc Open Source projects

Galois, Inc. (@GaloisInc)

GaloisInc

Stars
7,853
Global Org. Rank 2,924 (Top 1.0 %)
Registered about 12 years ago
Most used languages

Haskell
49.4 %

C
10.2 %

Rust
5.3 %

Python
5.3 %

C++
3.7 %

HTML
2.9 %

Java
2.4 %

JavaScript
2.4 %

Coq 2.4 %

TeX
2.0 %

Verilog 2.0 %

Shell
1.6 %

TypeScript
1.2 %

Jupyter Notebook
1.2 %

Others 7.6 %
Location 🇺🇸 United States
Country Total Rank 1,373
Country Ranking

Haskell
5

LLVM 6

Lean 7

SMT 8

Coq 26

ASL 53

Makefile 164

Racket
195

Verilog 226

Rust
231

TeX
334

OCaml
397

Assembly
583

Mathematica 586

C
1,002

C++
1,250

HTML
1,622

Dockerfile
1,855

Scala
2,070

Python
3,451

Jupyter Notebook
4,983

Shell
6,138

Java
7,556

JavaScript
8,005

cryptol

Cryptol: The Language of Cryptography

HaLVM

The Haskell Lightweight Virtual Machine (HaLVM): GHC running on Xen

crucible

Crucible is a library for symbolic simulation of imperative programs

saw-script

The SAW scripting language.

ivory

reopt

A tool for analyzing x86-64 binaries.

haskell-tor

A Haskell implementation of the Tor protocol.

swanky

A suite of rust libraries for secure multi-party computation

macaw

Open source binary analysis tools.

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.

what4

Symbolic formula representation and solver interaction library

HaNS

The haskell network stack

cclyzerpp

cclyzer++ is a precise and scalable pointer analysis for LLVM code.

cereal

ec2-unikernel

Tool for uploading unikernels into EC2

smaccmpilot-build

An umbrella repository including all of the dependencies to build the smaccmpilot project

dlkoopman

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

blt

Lattice-based integer linear programming solver

parameterized-utils

A set of utilities for using indexed types including containers, equality, and comparison.

grift

Galois RISC-V ISA Formal Tools

daedalus

The Daedalus data description language

saw-core

The SAW core language.

ddosflowgen

Simulate DDoS attacks and generate traffic datasets

minlibc

llvm-pretty-bc-parser

Parser for the llvm bitcode format

renovate

A library for binary analysis and rewriting

yapall

A precise and scalable pointer analysis for LLVM, written in Ascent

FreeRTOS-Xen

FreeRTOS 7.6.0 ported to run as a Xen guest on ARM systems.

hacrypto

Experiments in high-assurance crypto.

tower

A concurrency framework for the Ivory language

lean4-balance-car

Lean4 port of Arduino balance car controller

lean-protocol-support

This project contains various supporting libraries for lean to reason about protocols.

jvm-parser

A Haskell parser for JVM bytecode files

flexdis86

A library for disassembling x86-64 binaries.

halfs

The Haskell File System: A file system implementation in Haskell

elf-edit

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

mir-verifier

SAW front end for the MIR language from rustc

semmc

Stratified synthesis for learning machine code instruction semantics

fancy-garbling

Rust implementation of the BMR16 arithmetic garbling scheme.

smaccmpilot-stm32f4

SMACCMPilot flight controller

pure-zlib

A Haskell-only implementation of zlib / DEFLATE.

helib-demos

Experiments in homomorphic encryption

FiveUI

Extensible UI Analysis in your browser

lean-llvm

LLVM support for the lean theorem prover

galua

Lua debugger and interpreter

BESSPIN

Top-level repository including all relevant BESSPIN repository

curl

A Haskell binding to the curl library

json

Haskell JSON library

xml

Haskell XML library

estimator

State-space estimation algorithms and models

http-server

A Haskell HTTP server

dismantle

A library of assemblers and disassemblers derived from LLVM TableGen data

llvm-verifier

The LLVM Symbolic Simulator, part of SAW.

RSA

Haskell RSA Library

msf-haskell

Haskell implementation of Metasploit remote API

cryfsm

convert simple cryptol expressions into finite-state machines

lean-haskell-bindings

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

FAW

Galois Format Analysis Workbench

sqlite

A simple sqlite3 library for Haskell

BLST-Verification

BLST-Verification

cryptol-specs

A central repository for specifications of cryptographic algorithms in Cryptol

surveyor

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

mistral

An interpreter for the Mistral language.

LinearArbitrary-SeaHorn

LinearArbitrary-SeaHorn is a CHC solver for LLVM-based languages.

cryptol-semantics

Semantics for Cryptol

e2eviv

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

scuttlebutt

Multi-party computation utilities toolkit for rust

halvm-web

HARDENS

Repository for the HARDENS project

Jupyter Notebook

pads-haskell

A domain specific language for processing ad-hoc data.

ardupilot-mega

Fork: DO NOT SUBMIT PULL REQS/BUG REPORTS HERE

pate

Patches Assured up to Trace Equivalence

sat2015-crypto

Slides and examples to accompany the September 25th invited talk at SAT 2015

ICryptol

IPython-style interaction for Cryptol

reopt-vcg

A translation verifier for Reopt (https://github.com/GaloisInc/reopt)

ivory-tower-stm32

Tower backend and Ivory board support package for the STM32 line of microcontrollers

AMIDOL

Scientific model creation toolset.

hpb

Haskell Protocol Buffers

golang

Parser and type analysis for the Go programming language

mime

A Haskell MIME library

LIMA

LIMA: Language for Integrated Modeling and Analysis

gec

Embedded-friendly crypto a la SMACCM

SHA

Haskell implementation of SHA / SHA2 hash functions

alex-tools

A Haskell library making it easier to write Alex lexers.

nasa-affirm

Architectural Framework For Integrated Refinement Modeling

regex-fsm

Convert regular expressions into efficient matrix branching programs

salty

A DSL for generating GR(1) problems

simple-tar

A very simple tar archive processing library

ocelot

Oblivious transfer library for rust

hexdump

A human readable style for binary data.

gidl

Gidl: an Interface Description Language

saw-core-coq

A translator from SAWCore to Coq

BESSPIN-Voting-System-Demonstrator-2019

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

argo

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

lustre

A parser and AST for Lustre

rustwall

Rust firewall for seL4

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.

ivory-rtverification

Runtime verification for C code via a GCC plugin architecture.

BESSPIN-GFE-2019

The DARPA SSITH-funded Government Furnished Equipment on which all secure CPUs are based.

cryptol-verifier

The Cryptol Symbolic Simulator, part of SAW.