一种宽容的多线程程序内部时间信息流类型系统

It is proposed that a permissive type-based method for checking internal timing channel of multi-thread programs. We define a formal specification of non-interference based on the set of hidden-racing variables. Hidden threads are concerned specially in the type system, so that we can refine the analysis about the scene in which internal timing channel occurs. Furthermore, this system estimates the execution time of commands based on the operating type of target codes corresponding to the source codes, which makes the judgment about the execution time more accurate. Compared to those pre-proposed methods, type checking in this work will accept more codes actually secure, which means more permissive. In addition, the soundness of the type system is proved independent to the model of scheduler.