# data[].attributes.body
25% of algorithms submitted for FIPS validation had security flaws.

Source: http://csrc.nist.gov/groups/STM/cmvp/documents/CMVP2002/proceed/CMVP2603.pdf
This is partially because the mathematics in cryptographic papers necessarily looks very different from a highly optimized C program, so it's hard to notice discrepancies.

# data[].attributes.body
Copilot is a stream-based language for building real-time systems such as monitoring software for planes.
Real-time means that at all times, the system can react to some event in some fixed time.

Prattle is a tool to generate meaningless traffic in a network. This can cause a cyberattacker to make mistakes that make them easier to detect.

# data[].attributes.body
Galois develops tools for developing software that needs to as work intended, and only as intended, in a diverse set of areas such as cryptography, avionics, computer security, and human-computer interfaces.
Source: http://galois.com/about/

# data[].attributes.body
This corresponds directly to the SHA1 specification document!

# data[].attributes.body
f : ([8], [32], [32], [32]) -> [32]
f (t, x, y, z) =
  if (0 <= t)  && (t <= 19) then (x && y) ^ (~x && z)
   | (20 <= t) && (t <= 39) then x ^ y ^ z
   | (40 <= t) && (t <= 59) then (x && y) ^ (x && z) ^ (y && z)
   | (60 <= t) && (t <= 79) then x ^ y ^ z
   else error "f: t out of range"

Source: http://www.cryptol.net/index.html

# data[].attributes.body
SAW takes compiled C or Java code and translates it into a circuit representation.
Then it can use state-of-the-art SAT or SMT solvers (developed by others) to prove correctness.
Source: http://saw.galois.com/index.html

# data[].attributes.body
uint32_t ffs_musl (uint32_t x) {
  static const char debruijn32[32] = {
    0, 1, 23, 2, 29, 24, 19, 3, 30, 27, 25, 11, 20, 8, 4, 13, 31, 22, 28, 18, 26, 10, 7, 12, 21, 17, 9, 6, 16, 5, 15, 14
  };
  return x ? debruijn32[(x&-x)*0x076be629 >> 27]+1 : 0;
}

# data[].attributes.body
uint32_t ffs_ref(uint32_t word) {
    int i = 0;
    if(!word) return 0;
    for(int cnt = 0; cnt < 32; cnt++)
        if(((1 << i++) & word) != 0)
            return i;
    return 0; // notreached
}

# data[].attributes.body
Galois does Research and Development for the US Government

# data[].attributes.body
Cryptol is a language to express properties of programs in a very mathematical way.

This allows people to translate a cryptographic paper into a reference implementation. Then they can write their own implementation, and then use SAW to verify they're equivalent automatically.
More info: http://cryptol.net/

# data[].attributes.body
Are the following functions equivalent?

SAW proves this without help from humans.
Source: http://saw.galois.com/tutorial.html