%0 Journal Article
%T ChecKing Information Flow on Output Channel with Reachability Analysis of Pushdown System
基于下推系统可达性分析的输出信道信息流检测
%A SUN Cong
%A TANG Li-yong
%A CHEN Zhong
%A
孙 聪
%A 唐礼勇
%A 陈 钟
%J 计算机科学
%D 2011
%I
%X We proposed an approach for analyzing information-flow security of imperative language with output channels. The program is abstracted with pushdown system, which is then self-composed in order to adapt noninterference as a safety property. The output operations in the two relevant runs are respectively modeled as storing and matching procedure by pushdown rules. Then the termination-insensitive noninterference is verified by a reachability analysis of illegal-flow state. A variation of this approach can deal with program containing divergent run. An upper-bound regression algorithm was proposed to find the maximum upper-bound in order to trigger coercive termination of divergent run. The experimental results show that the approach is more precise and efficient than existing work.
%K Information f1ow
%K Noninterference
%K Pushdown system
%K Reachability analysis
信息流,不干涉性,下推系统,可达性分析
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=3FDBEA69C21D71CD5FDC23A87E0EB763&yid=9377ED8094509821&vid=16D8618C6164A3ED&iid=DF92D298D3FF1E6E&sid=89F76E117E9BDB76&eid=D767283A3B658885&journal_id=1002-137X&journal_name=计算机科学&referenced_num=0&reference_num=15