[lojikil.com]
Stefan Edwards (lojikil) is not presently logged in.
- Assurance Practice Lead, Trail of Bits
- Twitter/GitHub/Lobste.rs: lojikil
- Works in: Defense, FinTech, Blockchain, IoT, compilers,
vCISO services
- Previous: net, web, adversary sim, &c.
- Infosec philosopher, professional programming
language theorist, everyday agronomer, father.
WARNING: DEAF
WARNING: Noo Yawk
- cover what I've seen going from traditional infosec to high(er) assurance work
- talk about application of formal techniques & cryptography
- why none of this will save you, I'm still Eeyore
=> 
- TINSTAAFL: formal tools & cryptography aren't panaceas
- There is no golden road to
arithmeticsecurity - Formally proven code fails, fancy crypto breaks, OS setups can multiply problems
- OSINT, threat modeling, blackbox, web, net, lots of gov, finance
- those + formalisms, PLT, more exposure to fancy crypto
- design +
- denotation +
- formalized & verified model +
- centralized security controls +
- decentralized implementation ==
- "secure"
- Not much has changed
2016
- Java: Java Modeling Language (JML)
- C: Frama-C
- [fancy formal languages no one uses] : [fancy formal tools no one uses]
- Eiffel, Sather, Lissac, any other DBC language there
- TLA+, ACL2, &c were also alive
- Ada has been around since forever
- tools were verbose
- often unused, difficult to use, or unknown
- JML is > 20 years old (first specs & such from 1999)
- multiple compiler support it
- industry standard...
- "just" Hoare logic
- ... with large, longitudinal case studies...
- ... virtually unused
- regularly interact with formal tooling
- since joining ToB, have written two, one for a client
- ease of use has gotten better
- in Ethereum, there are many to chose from
- tend to lean towards ease of use vs specificity
- lots of verifiers, less specifiers
- more built in tests
contract_src="""
contract Adder {
function incremented(uint value) public
returns (uint){
if (value == 1)
revert();
return value + 1;
}
}
"""
# ...
value = m.make_symbolic_value()
contract_account.incremented(value)
# ...
for state in m.ready_states:
print("can value be 1? {}".format(
state.can_be_true(value == 1)))
- pros:
- much easier to start now
- multiple implementations, geared towards devs, CI/CD
- cons:
- the usual negatives
- as we'll see: formally proven/verified code can fail
- only as good as your spec/verification
- spec bugs
- under spec
- not spec'ing the right thing
- can't test everything
- tested code != prod code
- Ariane 5 rocket
- things look positive
- client proved with
uint, then switched toint
- client proved with
- lots of blockchain examples
from http://deniable.org/reversing/symbolic-execution
- SecLists
- Radamsa
- AFL
- QuickCheck (for Haskell), Hypothesis (Python)
- available, but unused
- some exotic stuff like DART
https://patricegodefroid.github.io/public_psfiles/talk-pldi2005.pdf
- those, plus
- easily accessible grammar fuzzers
- Mozilla Dharma, various others
- grey-box fuzzers
- ECLIPSER
- other combinations of symbex + fuzzing
- concretize via fuzzing
- negate paths ala SAGE
- property-based testing is much more common
- i still fine a ton of vulns with radamsa
radamsa -v -o $SOMEPATHis so stupidly effective
- property-based testing is p popular now
- allows developers to write simple properties that must hold
userIds <= 10000fromAddress != toAddress
- simple to write, often within the same language
- testing tool:
- generates random calls to API w/ random data
- shrinks random call graph to minimum
- all to find combinations that violate properties
contract TEST is NewCoin {
uint private initSupply;
address private alice = ...;
address private bob = ...;
address private eve = ...;
constructor() public {
balances[alice] = 10000;
balances[bob] = 10000;
balances[eve] = 10000;
initSupply = totalSupply_;
}
// the actual good stuff:
function echidna_test() public returns (bool) {
totalSupply_ = balances[alice] + balances[bob] +
balances[eve];
return (initSupply == totalSupply_);
}
}
- pros:
- can find many edge cases
- tools have become lightweight & easier to control
- cons
- unlikely to randomly generate complex formats
- anything > pure random takes time
- (more) ideal, combine constraint gen with fuzzing
- what you fuzz matters
- but so does how you fuzz
- as an aside, fuzzing, symbex, &c don't replace tests
- tests show expected result, intent
- fuzzing shows potential edge cases
- symbex, absint show domain/codomain
- both are useful
- mostly FIPS-140 types of stuff
- sometimes a rec for removing SHA
- use PBKDF2, bcrypt, scrypt
- pining to use SRP
- work with actual cryptographers
- lots and lots of math
- better systems
- libsodium, tink
SRPvarious PAKEs- Argon2
- Oblivious Functions
- so everything is better... right?
- keys written to disk with
0777or0655 - keys in memory that an attacker can access
- keys stored on GitHub
- lots of incorrect applications
- signature? hash? who knows!
- must. use. all. the. keys.
- I don't want to review it
- it's probably wrong
- you may not implement it correctly
- the library isn't audited
- we don't understand it
- zk-SNARKs
- mostly on prem
- Windows, Trusted Solaris, Linux
- some SELinux, some CAC access
- occassional orchestration, CM
- lots of orchestration
- almost 100% Linux
- containers == more security... right?
- ignoring simple docker failures
- k8s: by default disabled seccomp
- since fixed
- docker: multiple vulns, often used w/o a KSM
- gvisor: disabled seccomp
- must pay attention to defaults
- by themselves, not a security mechanism
- not worse, but false sense of security
- so you did everything right
- want a cookie?
- there are still a number of otherways to lose
- formally verify people?
- crypto your way around a hardware bug?
- SGX failures, k8s issues, &c.
- reduce your surface area
- employ full range of:
- threat modeling
- maturity modeling
- traditional SAST/DAST
- fuzzing
- design spec
- verification (appropos of your risk)
- someone commits prod keys to GH