Second European Symposium on Research in Computer Security (ESORICS 92)
Formal Methods and Automated Tool for Timing-Channel Identification in TCB Source Code
Jingsha He, Virgil D. Gligor
Keywords :
Abstract : We characterize the properties of timing channels that are reflected in source code and present formal methods for the identification of these channels in source code of trusted computing bases (TCBs). Our study differs significantly from previous ones which focus on a high-level characterization of timing channels without leading to practical methods for their identification. We also discuss how to integrate the formal methods presented into the automated system that has been previously developed for storage-channel identification to build an automated tool for timing-channel identification in TCB source code which, otherwise, is still carried out in an ad-hoc way due to the lack of general and practical methods. The presented methods, however, cannot be directly applied for detecting hardware channels that result from hardware system configurations.
(Pages 57-75)