User process does system call (trap). Protection: can't jump to arbitrary location. Restricted R/W/
Same restriction for mutually distrustful component (Adobe & MS). Want other side to crash, not this side.
Trusted code base: part of SW where bug could compromise security. Part you have to trust (whether you want to or not).
TCB
|
[]---|----[]
|
| []
|
| []
Different address spaces?
- socket, remote procedure call, create hole
- clumsy
- shared memory
Ken Thompson Turing Award speech.
- but hard to hide malicious code
- put in object code (a.out), not source
- put in lines to insert flaw into gcc when recompiled
Not enough to read source code.
Godel: some true statements do not have proofs.
Java type system: impossible to dereference arbitrary pointers. Can't see private data or jump to private methods.
Bugs: all SW has bugs (1 per 3000 lines for commercial SW).
Rice's thorem: avoid premises, avoid conclusion
Proof code: test theorems that must be true of code
- need to specify what you want to prove
- this is tough
Von Neumann: programmable computers. Set bits in memory (interesting side note: program just a series of integers).
Syntax: opcodes
Semantics: what an instructions does
Does proof prove theorem? (Given axioms, etc.) Have to trust axioms and proof checker.
Compile to assembly (gcc -s)
But what about Emacs? At some point, have to stop being paranoid.
Rice/Turing/Godel -> proofs about programs that came out of this compiler.
Problem with proving programs: how to specify? What is the spec of MS Word? To specify correctness, needs lots of domain knowledge. Proofs will be huge.
Solution: don't specify correctness, specify saftey.
- no domain of knowledge
- generate/check proof automatically.
