Logic of Multi-Threaded Programs for Non-Interference
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • 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
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:October 31,2012
  • Revised:October 31,2012
  • Adopted:
  • Online: May 30,2014
  • Published:
You are the firstVisitors
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