微信服务号

微信订阅号

2025-4-3- 17
Home > Archive>Volume 25, Issue 6, 2014 >1143-1153. DOI:10.13328/j.cnki.jos.004429
PDF HTML XML Export Cite reminder
Logic of Multi-Threaded Programs for Non-Interference
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [18]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    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.

    Reference
    [1] Smith G. Improved typings for probabilistic noninterference in a multi-threaded language. Journal of Computer Security, 2006,14(6):591-623.
    [2] Barthe G, Nieto LP. Formally verifying information flow type systems for concurrent and thread systems. In: Proc. of the 2004 ACM Workshop on Formal Methods in Security Engineering. Washington: ACM Press, 2004. 13-22. [doi: 10.1145/1029133.1029136]
    [3] Russo A, Hughes J, Naumann D, Sabelfeld A. Closing internal timing channels by transformation. In: Proc. of the 11th Asian Computing Science Conf. on Advances in Computer Science: Secure Software and Related Issues. Tokyo: Springer-Verlag, 2007.120-135. [doi: 10.1007/978-3-540-77505-8_10]
    [4] Sabelfeld A. The impact of synchronisation on secure information flow in concurrent programs. In: Bjφrner D, Broy M, Zamulin A,eds. Proc. of the 4th Int'l Andrei Ershov Memorial Conf. on Perspectives of System Informatics. Akademgorodok: Springer-Verlag,2001. 225-239.
    [5] Stevenc WR, Fenner B, Rudoff AM. UNIX Network Programming, Vol.1. 3rd ed., Beijing: China Machine Press, 2004. 121-151.
    [6] Dodds M, Feng XY, Parkinson M, Vafeiadis V. Deny-Guarantee reasoning. In: Castagna G, ed. Proc. of the Programming Languages and Systems. Berlin/Heidelberg: Springer-Verlag, 2009. 363-377. [doi: 10.1007/978-3-642-00590-9_26]
    [7] Feng XY. Local rely-guarantee reasoning. In: Proc. of the 36th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Savannah: ACM Press, 2009. 315-327. [doi: 10.1145/1480881.1480922]
    [8] Honda K, Vasconcelos V, Yoshida N. Secure information flow as typed process behaviour. In: Proc. of the 9th European Symp. on Programming Languages and Systems. Springer-Verlag, 2000. 180-199. [doi: 10.1007/3-540-46425-5_12]
    [9] Honda K, Yoshida N. A uniform type structure for secure information flow. ACM Trans. on Programming Languages System, 2007,29(6):31. [doi: 10.1145/1286821.1286822]
    [10] Mantel H, Sands D, Sudbrock H. Assumptions and guarantees for compositional noninterference. In: Proc. of the IEEE 24th Computer Security Foundations Symp. (CSF). IEEE, 2011. 218-232. [doi: 10.11.09/CSF.2011.22]
    [11] Mantel H, Sudbrock H. Flexible scheduler-independent security. In: Proc. of the 15th European Conf. on Research in Computer Security. Athens: Springer-Verlag, 2010. 116-133. [doi: 10.1007/978-3-642-15497-3_8]
    [12] Russo A, Sabelfeld A. Securing interaction between threads and the scheduler in the presence of synchronization. Journal of Logic and Algebraic Programming, 2009,78(7):593-618. [doi: 10.1016/j.jlap.2008.09.003]
    [13] Volpano D, Smith G. Probabilistic noninterference in a concurrent language. In: Proc. of the IEEE 11th Computer Security Foundations Workshop. IEEE, 1998. 34-43. [doi: 10.1109/CSFW.1998.683153]
    [14] Zdancewic S, Myers AC. Observational determinism for concurrent program security. In: Proc. of the IEEE 16th Computer Security Foundations Workshop. IEEE Press, 2003. 29-43. [doi: 10.1109/CSFW.2003.1212703]
    [15] Huisman M, Worah P, Sunesen K. A temporal logic characterisation of observational determinism. In: Proc. of the IEEE 19th Computer Security Foundations Workshop. IEEE Press, 2006. 1-13. [doi: 10.1099/CSFW.2006.6]
    [16] Stefan D, Russo A, Buiras P, Levy A, Mitchell JC, Mazières D. Addressing covert termination and timing channels in concurrent information flow systems. In: Proc. of the 17th ACM SIGPLAN Int'l Conf. on Functional Programming. Copenhagen: ACM Press,2012. 201-214. [doi: 10.1145/2364527.2364557]
    [17] Vaughan JA, Millstein T. Secure information flow for concurrent programs under total store order. In: Proc. of the IEEE 25th Computer Security Foundations Symp. (CSF). IEEE, 2012. 19-29. [doi: 10.1109/CSF.2012.20]
    [18] Krinke J. Context-Sensitive slicing of concurrent programs. SIGSOFT Software Engineering Notes, 2003,28(5):178-187. [doi:10.1145/940071.940096]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

李沁,曾庆凯,袁志祥.一种面向非干扰的线程程序逻辑.软件学报,2014,25(6):1143-1153

Copy
Share
Article Metrics
  • Abstract:3036
  • PDF: 4569
  • HTML: 1184
  • Cited by: 0
History
  • Received:October 31,2012
  • Revised:October 31,2012
  • Online: May 30,2014
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2032327Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063