Testing:
Demonstrate existence of problem
Cannot demonstrate absence of problem
Regression testing: ensure that alterations do not break existing functionality / performance
Challenges:
test case generation, code coverage, exponential number of different executions, different execution environments
Penetration testing:
Ethical hackers attempt to defeat security measures
Cannot demonstrate absence of problem
Formal verification: Checking a mathematical specification of program to ensure that security assertions hold.
– Model checking, automated theorem proving
– State variables w/initial assignment, program specification describing how state changes, boolean predicates over state variables
– Difficulty: exponential time & space worst case complexity
– Model checking pioneers won the 2007 turning award
Common Criteria(2005) international standard replaced orange book
– Originated out of European, Canadian, and US standards
– Idea: users specify system needs, vendors implement solution and make claims about security properties, evaluators determine whether vendors actually met claims
– Evaluation assurance level(EAL) rates systems
– EAL1 most basic, EAL7 most rigorous
