Logic of multi-threaded programs for non-interference

被引：0
作者：
Li, Qin [1 ]
Zeng, Qing-Kai [2 ,3 ]
Yuan, Zhi-Xiang [1 ]
机构：
[1] School of Computer, Anhui University of Technology
[2] State Key Laboratory for Novel Software Technology (Nanjing University)
[3] Department of Computer Science and Technology, Nanjing University
来源：
Ruan Jian Xue Bao/Journal of Software | 2014年 / 25卷 / 06期
关键词：
Axiomatic semantic; Dynamic scoping multi-threaded program; Non-interference;
D O I：
10.13328/j.cnki.jos.004429
中图分类号：
学科分类号：
摘要：
Existing work on the verification of information flow in threads mainly focuses on timing channels. However, this paper shows that system calls, such as 'fork' or 'join' with side effects, can also be used to create covert channels intentionally or accidentally. The study results in a dependency logic for verifying information flow in multi-threaded programs where improper calls over thread controlling primitives with side effects could incur illegal information flow. The logic can express the data flow, control flow and the side effects of thread-controlling system calls, and can reason about the dependency relationship among variables and thread identities, to determine whether secret variables interfere with public ones in multi-threaded programs. © 2014 ISCAS.
引用
收藏
页码：1143 / 1153
页数：10
相关论文
共 18 条
  • [1] Smith G., Improved typings for probabilistic noninterference in a multi-threaded language, Journal of Computer Security, 14, 6, pp. 591-623, (2006)
  • [2] Barthe G., Nieto L.P., Formally verifying information flow type systems for concurrent and thread systems, Proc. of the 2004 ACM Workshop on Formal Methods in Security Engineering, pp. 13-22, (2004)
  • [3] Russo A., Hughes J., Naumann D., Sabelfeld A., Closing internal timing channels by transformation, Proc. of the 11th Asian Computing Science Conf. on Advances in Computer Science: Secure Software and Related Issues, pp. 120-135, (2007)
  • [4] Sabelfeld A., The impact of synchronisation on secure information flow in concurrent programs, Proc. of the 4th Int'l Andrei Ershov Memorial Conf. on Perspectives of System Informatics, pp. 225-239, (2001)
  • [5] Stevenc W.R., Fenner B., Rudoff A.M., UNIX Network Programming, 1, pp. 121-151, (2004)
  • [6] Dodds M., Feng X.Y., Parkinson M., Vafeiadis V., Deny-Guarantee reasoning, Proc. of the Programming Languages and Systems, pp. 363-377, (2009)
  • [7] Feng X.Y., Local rely-guarantee reasoning, Proc. of the 36th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pp. 315-327, (2009)
  • [8] Honda K., Vasconcelos V., Yoshida N., Secure information flow as typed process behaviour, Proc. of the 9th European Symp. on Programming Languages and Systems, pp. 180-199, (2000)
  • [9] Honda K., Yoshida N., A uniform type structure for secure information flow, ACM Trans. on Programming Languages System, 29, 6, (2007)
  • [10] Mantel H., Sands D., Sudbrock H., Assumptions and guarantees for compositional noninterference, Proc. of the IEEE 24th Computer Security Foundations Symp. (CSF). IEEE, pp. 218-232, (2011)
12