TY - GEN
T1 - Information flow analysis for a typed assembly language with polymorphic stacks
AU - Bonelli, Eduardo
AU - Compagnoni, Adriana
AU - Medel, Ricardo
PY - 2006
Y1 - 2006
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=33745821985&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33745821985&partnerID=8YFLogxK
U2 - 10.1007/11741060_3
DO - 10.1007/11741060_3
M3 - Conference contribution
AN - SCOPUS:33745821985
SN - 3540336893
SN - 9783540336891
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 37
EP - 56
BT - Construction and Analysis of Safe, Secure, and Interoperable Smart Devices - Second International Workshop, CASSIS 2005, Revised Selected Papers
T2 - 2nd International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS 2005
Y2 - 8 March 2005 through 11 March 2005
ER -