Show simple item record

dc.contributor.advisorSteel, Graham
dc.contributor.advisorAspinall, David
dc.contributor.advisorStark, Ian
dc.contributor.authorKeighren, Gavin
dc.date.accessioned2014-06-20T15:17:38Z
dc.date.available2014-06-20T15:17:38Z
dc.date.issued2014-06-27
dc.identifier.urihttp://hdl.handle.net/1842/8963
dc.description.abstractSecurity APIs are designed to enable the storage and processing of confidential data without that data becoming known to individuals who are not permitted to obtain it, and are central to the operation of Automated Teller Machines (ATM) networks, Electronic Point of Sale (EPOS) terminals, set-top boxes for subscription-based TV, pre-payment utility meters, and electronic ticketing for an increasing number of public transport systems (e.g., Oyster in London). However, since the early 2000s, it has become clear that many of the security APIs in widespread use contain subtle flaws which allow malicious individuals to subvert the security restrictions and obtain confidential data that should be protected. In this thesis, we attempt to address this problem by presenting a type system in which specific security properties are guaranteed to be enforced by security APIs that are well-typed. Since type-checking is a form of static analysis, it does not suffer from the scalability issues associated with approaches that simulate interactions between a security API and one or more malicious individuals. We also show how our type system can be used to model an existing security API and provide the same guarantees of security that the API authors proved it upholds. This result follows directly from producing a well-typed implementation of the API, and demonstrates how our type system provides security guarantees without requiring additional API-specific proofs.en_US
dc.contributor.sponsorEngineering and Physical Sciences Research Council (EPSRC)en_US
dc.language.isoenen_US
dc.publisherThe University of Edinburghen_US
dc.relation.hasversionV. Cortier, G. Keighren, and G. Steel. Automatic Analysis of the Security of XORBased Key Management Schemes. In O. Grumberg and M. Huth, editors, Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2007), number 4424 in Lecture Notes in Computer Science, pages 538–552. Springer-Verlag, Mar. 2007.en_US
dc.relation.hasversionG. Keighren. Model Checking Security APIs. Master’s thesis, School of Informatics, University of Edinburgh, Aug. 2006. Available online at http://www.inf.ed.ac. uk/publications/thesis/online/IM060368.pdf.en_US
dc.subjectsecurity APIsen_US
dc.subjectinformation flowen_US
dc.subjecttype systemen_US
dc.subjectnon-interferenceen_US
dc.titleRestricting information flow in security APIs via typingen_US
dc.typeThesis or Dissertationen_US
dc.type.qualificationlevelDoctoralen_US
dc.type.qualificationnamePhD Doctor of Philosophyen_US


Files in this item

This item appears in the following Collection(s)

Show simple item record