| Popis: |
We present the first methodology for analysis and automated detection of attacks on security application programming interfaces (security APIs) – the interfaces to hardware cryptographic services used by developers of critical security systems, such as banking applications. Taking a cue from previous work on the formal analysis of security protocols, we model APIs purely according to specifications, under the assumption of ideal encryption primitives. We use a theorem prover tool and adapt it to the security API context. We develop specific formalization and automation techniques that allow us to fully harness the power of a theorem prover. We show how, using these techniques, we were able to automatically re-discover all of the pure API attacks originally documented by Bond and Anderson against banking payment networks, since their discovery of this type of attack in 2000. We conclude with a note of encouragement: the complexity and unintuiveness of the modelled attacks make a very strong case for continued focus on automated formal analysis of cryptographic APIs. |
