More Typed Assembly Languages for Confidentiality

We propose a series of type systems for the information-flow security of assembly code. These systems extend previous work TALC with some timing annotations and associated judgments and rules. By using different timing rules, these systems are applicable to different practical settings. In particular, they can be used to prevent illicit information flow through the termination and timing channels in sequential programs as well as the possibilistic and probabilistic channels in multi-threaded programs. We present the formal details of these as a generic type system TAL+ C and prove its noninterference. TAL+ C is designed as a core target language for certifying compilation. We illustrate its use with a formal scheme of type-preserving translation.

• Type: Conference
• Year: 2007
• Where: APLAS
• Authors: Dachuan Yu
• Keywords: APLAS 2007, Programming Languages, Timing Annotations, Timing Channels, Type System