Analysis of Security APIs FAQ

Graham Steel

Basics

  1. What is a security API?

    A security API allows untrusted code to access sensitive resources in a secure way. It is the interface between processes running with different levels of trust. Examples of security APIs include the interface between the tamper-resistant chip on a smartcard (trusted) and the card reader (untrusted), the interface between a cryptographic Hardware Security Module (trusted) and the client machine (untrusted), and the Google maps API (an interface between a server, trusted by Google, and the rest of the Internet).

    The crucial aspect of a security API is that it is designed to enforce a policy, i.e. no matter what sequence of commands in the interface are called, and no matter what the parameters, certain security properties should continue to hold. This means that if the less trusted code turns out to be malicious (or just faulty), the carefully designed API should prevent compromise of critical data.

    For a full introduction to the subject, see chapter 18 of Anderson's Security Engineering [1, Chapter 18], which is available online.

  2. Is a security API the same thing as a cryptographic API?

    No, we consider a cryptographic API to just provide cryptographic functionality. A crypto API becomes a security API when it is designed to enforce a policy, i.e. that no matter what sequence of commands in the interface are called, certain `good properties' remain true. In the case of a cryptographic API, the property might be that the true value of sensitive keys remains unknown to the calling application.

  3. Is a security API the same thing as a security protocol?

    No, though they are closely related. Security protocols are short programs that describe how principals may communicate securely over an insecure network, usually using cryptography. If one considers the (possibly malicious) calling application to be the untrusted network, the security API can be considered to be a set of protocols, which the malicious application might call in any order to effect an attack.

Security API attacks

  1. What is an API attack?

    An API attack is a sequence of commands which breaks the security policy of the interface.

  2. Do real API attacks exist?

    Yes, many. See for example the work of Longley and Rigby [16], Anderson & Bond, [4] Bond [3], Clayton and Bond [5], Clulow [6,7], Berkman and Ostrovsky [2], Cortier & Keighren & Steel [9], and Delaune & Kremer & Steel [11].

    These attacks are not just academic examples - attacks on the APIs of Hardware Security Modules (HSMs) used in the cash machine network have been used in large scale fraud (see for example this Wired article). As a result of attacks like these, the Payment Card Industry (PCI) standard for HSMs (April 2009) now mandates the absence of such attacks (see requirement B9 here - "The HSM's functionality shall not be influenced by logical anomalies such as (but not limited to) unexpected command sequences, unknown commands, commands in a wrong device mode and supplying wrong parameters or data which could result in the HSM outputting the clear-text PIN or other sensitive information."

  3. Are all these attacks similar? Can they be classified?

    These attacks differ in particular in the amount of off-line (i.e. not talking to the API) brute force cryptanalysis that is required to complete the attack. Some authors distinguish between a `pure API attack' or `logical attack', where all the attacker needs to do is send commands and do some trivial processing on the output, and other kinds of API attack, where some degree of brute-force cryptanalysis is required.

Formal API analysis

  1. What is formal security API analysis?

    In formal security analysis, we use the techniques of mathematical logic to model an API, its security policy, and an attacker, and try to find (or prove the absence of) certain classes of attack. This idea comes from existing work in formal analysis of security protocols, which itself is related to formal program analysis.

  2. What methods have been used for formal API analysis?

    Generally, researchers have first constructed abstract models of APIs and the attacker following the approach of Dolev and Yao [12]. These models are typically constructed `by hand' from the API specification, and are written in some logic such as first-order Horn clauses or rewrite rules. The search for an attack usually consists of the testing to see if some secret term can become known to the intruder. This can be mechanised as the reachability of a certain state an model checker, or the derivability of a certain term in an automated theorem prover [18,20,10,9,8,19].

    Another method that has been used in particular for PIN processing APIs involves modelling the API and the intruder as a Markov decision process, and looking for attacks with the probabilistic model checker PRISM. You can read more about that on the PRISM case-study page.

  3. Does formal API analysis give us any useful results?

    Yes, formal API analysis has lead to the discovery of new attacks, e.g. [14,11,15], and some proofs of security e.g. [10,9,2,3,1].

  4. Isn't formal API analysis just the same as security protocol analysis?

    It is similar, but typically throwing an API problem at a security protocol analyser produces poor results. The reasons are:

    Security API models typically contain global non-monotonic mutable state, which much be modelled accurately to get reasonable precision (i.e. not too many false attacks).

    Security APIs typically consist of many dozens of functions which may be called in any order. Security protocols usually consist of half a dozen or so messages in a given sequence. Thus the abstractions which can be used to keep the search space manageable, and the search techniques and tools, are different. APIs usually include several commands which share the same cryptographic keys, which is problematic for composition results which would allow the comands to me analysed in a more modular way.

    In API analysis we are typically interested in concrete implementations using particular cryptographic algorithms which may have algebraic properties and susceptibility to certain brute-force attacks. In security protocol analysis we typically assume cryptographic functions are `perfect' or at least IND-CCA. This assumption might not be applicable to APIs used in e.g. pay TV decoders or low power smartcards.

  5. Isn't formal API analysis just the same as the analysis of implementations of security protocols?

    It is a close match - you can regard the code implementing Alice's role in a protocol as offering a security API. If we carry out the analysis with `holes' in the code for arbitrary untrusted code, a la Myers et al [17] we can imagine the holes being filled by the malicious calling application. This is the approach used e.g. by Fournet et al. There are differences though, and not just in scale: in API analysis, we are often concerned with low level key-management commands, i.e. generating, exporting, importing and using keys, possibly to encrypt other keys. Protocols implementation analysis typically excludes these operations (e.g [13]).

Finding out more

  1. Is there a successful international workshop series on API analysis?

    Yes

  2. What papers can I read about API analysis?

    Below is my bibliography on API analysis - this is fairly large but by no means complete.

Bibliography

1
R. Anderson.
Security Engineering.
Wiley, 2nd edition, 2007.

2
O. Berkman and O. M. Ostrovsky.
The unbearable lightness of pin cracking.
In Financial Cryptography and Data Security (FC), Scarborough, Trinidad and Tobago, February 2007.

3
M. Bond.
Understanding Security APIs.
PhD thesis, University of Cambridge, 2004.

4
M. Bond and R. Anderson.
API level attacks on embedded systems.
IEEE Computer Magazine, 34(10):67-75, October 2001.

5
C. Cachin and N. Chandran.
A secure cryptographic token interface.
In Computer Security Foundations (CSF-22), Long Island, New York, 2009. IEEE Computer Society Press.

6
R. Clayton and M. Bond.
Experience using a low-cost FPGA design to crack DES keys.
In Cryptographic Hardware and Embedded System - CHES 2002, pages 579-592, 2002.

7
J. Clulow.
The design and analysis of cryptographic APIs for security devices.
Master's thesis, University of Natal, Durban, 2003.

8
J. Clulow.
On the security of PKCS#11.
In Proceedings of CHES 2003, pages 411-425, 2003.

9
V. Cortier, S. Delaune, and G. Steel.
A formal theory of key conjuring.
In Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSF20), pages 79-93, Venice, Italy, 2007.

10
V. Cortier, G. Keighren, and G. Steel.
Automatic analysis of the security of XOR-based key management schemes.
In O. Grumberg and M. Huth, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), number 4424 in LNCS, pages 538-552, 2007.

11
Véronique Cortier and Graham Steel.
A generic security API for symmetric key management on cryptographic devices.
In Michael Backes and Peng Ning, editors, Proceedings of the 14th European Symposium on Research in Computer Security (ESORICS'09), volume 5789 of Lecture Notes in Computer Science, pages 605-620, Saint Malo, France, September 2009. Springer.

12
J. Courant and J.-F. Monin.
Defending the bank with a proof assistant.
In Proceedings of the 6th International Workshop on Issues in the Theory of Security (WITS'06), pages 87 - 98, Vienna, Austria, March 2006.

13
S. Delaune, S. Kremer, and G. Steel.
Formal analysis of PKCS#11.
In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF'08), pages 331-344, Pittsburgh, PA, USA, June 2008. IEEE Computer Society Press.

14
D. Dolev and A. Yao.
On the security of public key protocols.
IEEE Transactions in Information Theory, 2(29):198-208, March 1983.

15
C. Fournet and T. Rezk.
Cryptographically sound implementations for typed information-flow security.
In POPL, pages 323-335, 2008.

16
S. Fröschle and G. Steel.
Analysing PKCS#11 key management APIs with unbounded fresh data.
In P. Degano and L. Viganò, editors, Preliminary Proceedings of the Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS'09), volume 5511 of Lecture Notes in Computer Science, pages 92-106, York, UK, 2009. Springer.
To appear.

17
G. Keighren.
Model checking security APIs.
Master's thesis, University of Edinburgh, 2007.

18
R. Küsters and T. Truderung.
Reducing Protocol Analysis with XOR to the XOR-free Case in the Horn Theory Based Approach.
In Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS 2008), pages 129-138. ACM Press, 2008.

19
D. Longley and S. Rigby.
An automatic search for security flaws in key management schemes.
Computers and Security, 11(1):75-89, March 1992.

20
A. Myers, A. Sabelfeld, and S. Zdancewic.
Enforcing robust declassification and qualified robustness.
Journal of Computer Security, 14(2):157-196, 2006.

21
G. Steel.
Deduction with XOR constraints in security API modelling.
In R. Nieuwenhuis, editor, Proceedings of the 20th Conference on Automated Deduction (CADE 20), number 3632 in Lecture Notes in Artificial Intelligence, pages 322-336, Tallinn, Estonia, July 2005. Springer-Verlag Heidelberg.

22
E. Tsalapati.
Analysis of PKCS#11 using AVISPA tools.
Master's thesis, University of Edinburgh, 2007.

23
P. Youn, B. Adida, M. Bond, J. Clulow, J. Herzog, A. Lin, R. Rivest, and R. Anderson.
Robbing the bank with a theorem prover.
Technical Report UCAM-CL-TR-644, University of Cambridge, August 2005.