Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Information Flow Analysis for a Typed Assembly Language with Polymorphic Stacks

Eduardo BonelliContact Information, Adriana CompagnoniContact Information and Ricardo MedelContact Information

(1)  LIFIA, Fac. de Informática, Univ. Nac. de La Plata, Argentina
(2)  Stevens Institute of Technology, Hoboken NJ 07030, USA
Abstract
We study secure information flow in a stack based Typed Assembly Language (TAL). We define a TAL with an execution stack and establish the soundness of its type system by proving non-interference. One of the problems of studying information flow for a low-level language is the absence of high-level control flow constructs that guide information flow analysis in high-level languages. Furthermore, in the presence of an execution stack, code that frees space on the stack must be constrained in order to avoid illegal flows. Finally, in the presence of stack polymorphism, we must ensure that type variables are instantiated without observable differences. These issues are addressed by introducing junction points into the type system, ensuring that they behave as ordered linear continuations, and that they interact safely with the execution stack. We also discuss several limitations of our approach and point out some remaining open issues.

Contact Information Eduardo Bonelli
Email: eduardo@sol.info.unlp.edu.ar

Contact Information Adriana Compagnoni
Email: abc@cs.stevens.edu

Contact Information Ricardo Medel
Email: rmedel@cs.stevens.edu
Fulltext Preview (Small, Large)
Image of the first page of the fulltext


Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.113 • Server: mpweb18
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)