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

计算机科学 ›› 2014, Vol. 41 ›› Issue (3): 163-168.

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

李沁,袁志祥

安徽工业大学计算机学院马鞍山243032;安徽工业大学计算机学院马鞍山243032

出版日期:2018-11-14 发布日期:2018-11-14
基金资助:
本文受国家自然科学基金(61170070)资助

Permissive Type System for Internal Timing Information Flow in Multi-thread Programs

LI Qin and YUAN Zhi-xiang

Online:2018-11-14 Published:2018-11-14

摘要/Abstract

摘要： 提出了一种针对多线程程序的内部时间信息流的宽容的类型系统。在隐藏竞争变量集合的基础上定义了非干扰属性的形式化规范;在类型系统中区分了隐藏线程,细化了对内部时间信息流发生场景的分析。相对于已有的基于类型理论的方法,本类型系统可以允许更多实质上安全的代码通过类型检查。另外,类型系统的可靠性是在独立于调度模型的情况下证明的。

关键词: 非干扰,内部时间信道,类型理论中图法分类号TP301文献标识码A

Abstract: This paper proposed a permissive type theory for checking internal timing channels in multi-thread programs．A formal specification of non-interference was defined based on the set of hidden-racing variables．In the type system,threads were discriminated according to the ways by which they deal with low level variables,so that we could refine the analysis about the scenario in which internal timing channel occurs．In contrast to existing methods,type checking in this work is more permissive because of less false positive．In addition,the soundness of the type system is proved in independent of the scheduler model.

Key words: Non-interference,Internal timing channel,Type theory

李沁,袁志祥. 一种宽容的多线程程序内部时间信息流类型系统[J]. 计算机科学, 2014, 41(3): 163-168. https://doi.org/

LI Qin and YUAN Zhi-xiang. Permissive Type System for Internal Timing Information Flow in Multi-thread Programs[J]. Computer Science, 2014, 41(3): 163-168. https://doi.org/

参考文献

[1] Sabelfeld A,Myers A C．Language-based information-flow security[J]．IEEE Journal on Selected Areas in Communications,2003,21(1):5-19
[2] Smith G.Improved typings for probabilistic noninterference in a multi-threaded language[J].J．Comput．Secur.,2006,14(6):591-623
[3] Russo A,et al．Closing internal timing channels by transformation[C]∥Proceedings of the 11th Asian computing science conference on Advances in computer science:secure software and related issues 2007．Tokyo,Japan:Springer-Verlag,2007
[4] Terauchi T．A Type System for Observational Determinism[C]∥Computer Security Foundations Symposium,2008．CSF ’08．IEEE 21st．2008
[5] Russo A,Sabelfeld A．Securing interaction between threads and the scheduler in the presence of synchronization[J]．Journal of Logic and Algebraic Programming,2009,78(7):593-618
[6] Zdancewic S,Myers A C．Observational determinism for concurrent program security[C]∥Computer Security Foundations Workshop 2003．Proceedings 16th IEEE．2003
[7] Sabelfeld A.The Impact of Synchronisation on Secure Information Flow in Concurrent Programs[C]∥Revised Papers from the 4th International Andrei Ershov Memorial Conference on Perspectives of System Informatics．Akademgorodok,Novosi-birsk,Russia:Springer-Verlag,2001:225-239
[8] Volpano D,Smith G．Probabilistic noninterference in a concur-rent language[C]∥Computer Security Foundations Workshop 1998．Proceedings 11th IEEE．1998
[9] Huisman M,Worah P,Sunesen K．A temporal logic characteri-sation of observational determinism[C]∥Proceedings of the 19th IEEE Workshop on Computer Security Foundations．2006
[10] Mantel H,Sands D,Sudbrock H．Assumptions and Guarantees for Compositional Noninterference[C]∥Computer Security Foundations Symposium 2011IEEE 24th．2011
[11] Boudol G,Castellani I．Noninterference for concurrent programs and thread systems[J]．Theoretical Computer Science,2002,281(1/2):109-130
[12] Barthe G,Nieto L P．Formally verifying information flow type systems for concurrent and thread systems[C]∥Proceedings of the 2004ACM Workshop on Formal Methods in Security Engineering 2004．ACM:Washington DC,USA,2004:13-22

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed