Notes on proof of attack vs proof of security

proof-of-attack_vs_proof-of-security.txt

Proof of attack vs proof of security

Soundness (NO false positives, may false negatives)
- May miss out legitimate cases
- "Conservative" systems normally at least have soundness
Completeness (may false positives, NO false negatives)
- Never miss out legitimate cases, but may grab more than needed

Proof of attack (off sec)
- Under some premises, shows there exists an attack for a given system (e.g. protocol, software)
- Soundness of the anaylsis method/procedure/algorithm/function (we name it said procedure f, and system s):
  - f is sound if:
    - If f(s) says there is an attack, then there IS an attack
- From soundness alone:
  - If f(s) does NOT say there is an attack (e.g. returned false, does not terminate, etc),
    then all bets are off if we only have soundness
  - Failure to find an attack does NOT imply the system is secure in the general case (cause Halting problem),
    i.e. failure to find an attack does not suffice as proof of security in the general case
- Completeness of f:
  - f is complete if:
    - If there is an attack, then f(s) will find it
- From completeness alone:
  - If f(s) provides an attack, it may not be an actual attack (i.e. false positive)
  - Success in finding an attack does NOT imply there is an attack in the general case
- Sound+complete:
  - Then f(s) provides an attack if and only if there is an attack for s
    - Exactly zero false negatives and exactly zero false positives
    - Not possible in the general case, cause Halting problem

Proof of security (def sec)
- Under some premises, shows there exists no attack for a given system
- Under some premises, shows that negligible probability of a successful attack for a given system
- Soundness of the anaylsis method/procedure/algorithm/function (we name it said procedure f, and system s):
  - f is sound if the following conditions are met:
    - If f(s) says s is secure, then there are NO attacks
- From soundness alone:
  - If f(s) does NOT say s is secure (e.g. returned false, does not terminate, etc),
    then all bets are off
  - Failure to provide a proof of security does NOT imply there is an attack in the general case (cause Halting problem),
    i.e. failure to prove s is secure does not suffice as a proof of attack
- Completeness of f:
  - f is complete if:
    - If there are no attacks for s, then f(s) will provide a proof of security
- From completeness alone:
  - If f(s) provides a proof of security, it may not be actually secure (over confidence)
  - Success in coming up with a proof of security does NOT imply there are no attacks in the general case
- Sound+complete:
  - Then f(s) provides a proof of security if and only if there are not attacks for s
    - Exactly zero false negatives and exactly zero false positives
    - Not possible in the general case, cause Halting problem

Antivirus:
- Neither sound nor complete, whether we consider it from proof of attack standpoint or proof of security standpoint

For security engineers:
- Solution exists if there is a "good enough" procedure (e.g. best effort, heuristics-based methods)

For formal methods people:
- Solution exists if there is a sound procedure

Virustotal:
- Still neither sound nor complete