Towards a Type System for Security APIs (bibtex)
by Gavin Keighren, David Aspinall, Graham Steel
Abstract:
Security API analysis typically only considers a subset of an API's functions, with results bounded by the number of function calls. Furthermore, attacks involving partial leakage of sensitive information are usually not covered. Type-based static analysis has the potential to alleviate these shortcomings. To that end, we present a type system for secure information flow based upon the one of Volpano, Smith and Irvine, extended with types for cryptographic keys and ciphertext similar to those in Sumii and Pierce. In contrast to some other type systems, the encryption and decryption of keys does not require special treatment. We show that a well-typed sequence of commands is non-interferent, based upon a definition of indistinguishability where, in certain circumstances, the adversary can distinguish between ciphertexts that correspond to encrypted public data.
Reference:
Towards a Type System for Security APIs (Gavin Keighren, David Aspinall, Graham Steel), In Revised Selected Papers of the Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS'09) (Pierpaolo Degano, Luca Viganò, eds.), Springer, volume 5511, 2009.
Bibtex Entry:
@inproceedings{KAS-arspawits09,
  abstract =      {Security API analysis typically only considers a
                   subset of an API's functions, with results bounded by
                   the number of function calls. Furthermore, attacks
                   involving partial leakage of sensitive information
                   are usually not covered. Type-based static analysis
                   has the potential to alleviate these shortcomings. To
                   that end, we present a type system for secure
                   information flow based upon the one of Volpano, Smith
                   and Irvine, extended with types for cryptographic
                   keys and ciphertext similar to those in Sumii and
                   Pierce. In~contrast to some other type systems, the
                   encryption and decryption of keys does not require
                   special treatment. We show that a well-typed sequence
                   of commands is non-interferent, based upon a
                   definition of indistinguishability where, in certain
                   circumstances, the adversary can distinguish between
                   ciphertexts that correspond to encrypted public
                   data.},
  address =       {York, UK},
  author =        {Keighren, Gavin and Aspinall, David and
                   Steel, Graham},
  booktitle =     {{R}evised {S}elected {P}apers of the {J}oint
                   {W}orkshop on {A}utomated {R}easoning for {S}ecurity
                   {P}rotocol {A}nalysis and {I}ssues in the {T}heory of
                   {S}ecurity ({ARSPA-WITS}'09)},
  DOI =           {10.1007/978-3-642-03459-6_12},
  editor =        {Degano, Pierpaolo and Vigan{\`o}, Luca},
  month =         aug,
  pages =         {173-192},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {Towards a Type System for Security {API}s},
  volume =        {5511},
  year =          {2009},
  acronym =       {{ARSPA-WITS}'09},
  nmonth =        {8},
  conf-year =     {2009},
  conf-month =    mar,
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KAS-arspawits09.pdf},
  PDF =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KAS-arspawits09.pdf},
  lsv-category =  {intc},
  wwwpublic =     {public and ccsb},
}
Powered by bibtexbrowser