%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