Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Formalizing a secure foreign function interface
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
2015 (English)In: Software Engineering and Formal Methods, Springer, 2015, 215-230 p.Conference paper, Published paper (Refereed)
Abstract [en]

Many high-level functional programming languages provide programmers with the ability to interoperate with untyped and low-level languages such as C and assembly. Research into the security of such interoperation has generally focused on a closed world scenario, one where both the high-level and low-level code are defined and analyzed statically. In practice, however, components are sometimes linked in at run-time through malicious means. In this paper we formalize an operational semantics that securely combines MiniML, a light-weight ML, with a model of a low-level attacker, without relying on any static checks on the attacker. We prove that the operational semantics are secure by establishing that they preserve and reflect the equivalences of MiniML. To that end a notion of bisimulation for the interaction between the attacker and MiniML is developed.

Place, publisher, year, edition, pages
Springer, 2015. 215-230 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9276
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-267089DOI: 10.1007/978-3-319-22969-0_16ISI: 000365046400016ISBN: 978-3-319-22968-3 (print)OAI: oai:DiVA.org:uu-267089DiVA: diva2:872009
Conference
13th International Conference on Software Engineering and Formal Methods (SEFM), September 7–11, York, UK
Available from: 2015-08-21 Created: 2015-11-17 Last updated: 2016-02-09Bibliographically approved

Open Access in DiVA

fulltext(455 kB)33 downloads
File information
File name FULLTEXT01.pdfFile size 455 kBChecksum SHA-512
0f110b6e076a1ec3c93a3794207a259cb3b1850090aa108709eaf8de9b3e17892528620074fd8921b156929db2108cbaf9d4203d6c4e87e5052b872fdba6fa41
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Authority records BETA

Larmuseau, AdriaanClarke, Dave

Search in DiVA

By author/editor
Larmuseau, AdriaanClarke, Dave
By organisation
Computing Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 33 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 302 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf