{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:31:51Z","timestamp":1750221111735,"version":"3.41.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T00:00:00Z","timestamp":1540339200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1566411, CNS-1702760, CNS-1816282"],"award-info":[{"award-number":["CCF-1566411, CNS-1702760, CNS-1816282"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,10,24]]},"abstract":"<jats:p>Dependent security labels (security labels that depend on program states) in various forms have been introduced to express rich information flow policies. They are shown to be essential in the verification of real-world software and hardware systems such as conference management systems, Android Apps, a MIPS processor and a TrustZone-like architecture. However, most work assumes that all (complex) labels are provided manually, which can both be error-prone and time-consuming.<\/jats:p>\n          <jats:p>In this paper, we tackle the problem of automatic label inference for static information flow analyses with dependent security labels. In particular, we propose the first general framework to facilitate the design and validation (in terms of soundness and\/or completeness) of inference algorithms. The framework models label inference as constraint solving and offers guidelines for sound and\/or complete constraint solving. Under the framework, we propose novel constraint solving algorithms that are both sound and complete. Evaluation result on sets of constraints generated from secure and insecure variants of a MIPS processor suggests that the novel algorithms improve the performance of an existing algorithm by orders of magnitude and offers better scalability.<\/jats:p>","DOI":"10.1145\/3276485","type":"journal-article","created":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T11:57:18Z","timestamp":1540382238000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["A derivation framework for dependent security label inference"],"prefix":"10.1145","volume":"2","author":[{"given":"Peixuan","family":"Li","sequence":"first","affiliation":[{"name":"Pennsylvania State University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Danfeng","family":"Zhang","sequence":"additional","affiliation":[{"name":"Pennsylvania State University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00007-6"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.177847"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2012.22"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289451"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00023"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806643"},{"volume-title":"Proc. European Symposium on Programming (ESOP). 520\u2013535","author":"Condit Jeremy","key":"e_1_2_1_8_1"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/17.2.143"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037739"},{"volume-title":"Proc. IEEE Symp. on Security and Privacy (S&amp;P). 11\u201320","author":"Joseph","key":"e_1_2_1_11_1"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_5"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111045"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411212"},{"volume-title":"Monitoring Information Flow. In Workshop on Foundations of Computer Security - FCS\u201905","year":"2005","author":"Guernic Gurvan Le","key":"e_1_2_1_15_1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.17"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629606"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676994"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.36"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292561"},{"key":"e_1_2_1_23_1","unstructured":"Andrew C. Myers G. Edward Suh Danfeng Zhang Yao Wang Andrew Ferraiuolo Rui Xu and Ian Thompson. 2015. SecVerilog 1.0: Verilog + Information Flow. (2015). Software release http:\/\/www.cs.cornell.edu\/projects\/secverilog .  Andrew C. Myers G. Edward Suh Danfeng Zhang Yao Wang Andrew Ferraiuolo Rui Xu and Ian Thompson. 2015. SecVerilog 1.0: Verilog + Information Flow. (2015). Software release http:\/\/www.cs.cornell.edu\/projects\/secverilog ."},{"key":"e_1_2_1_24_1","unstructured":"Andrew C. Myers Lantian Zheng Steve Zdancewic Stephen Chong and Nathaniel Nystrom. 2006. Jif 3.0: Java Information Flow. (July 2006). Software release http:\/\/www.cs.cornell.edu\/jif .  Andrew C. Myers Lantian Zheng Steve Zdancewic Stephen Chong and Nathaniel Nystrom. 2006. Jif 3.0: Java Information Flow. (July 2006). Software release http:\/\/www.cs.cornell.edu\/jif ."},{"key":"e_1_2_1_25_1","unstructured":"Nadia Polikarpova Jean Yang Shachar Itzhaky Travis Hance and Armando Solar-Lezama. 2018. Enforcing Information Flow Policies with Type-Targeted Program Synthesis. arXiv preprint arXiv:1607.03445v2 (2018).  Nadia Polikarpova Jean Yang Shachar Itzhaky Travis Hance and Armando Solar-Lezama. 2018. Enforcing Information Flow Policies with Type-Targeted Program Synthesis. arXiv preprint arXiv:1607.03445v2 (2018)."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503302"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00011-8"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11486-1_30"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.20"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2008.29"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1290520.1290526"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.20"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628161"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/353629.353648"},{"volume-title":"Proc. IEEE Symposium on Logic in Computer Science. 375\u2013387","year":"2000","author":"Xi Hongwei","key":"e_1_2_1_38_1"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535870"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694372"},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Lantian Zheng and Andrew C. Myers. 2007. Dynamic Security Labels and Static Information Flow Control. Intl\u2019 J. of Information Security 6 2\u20133 (March 2007).   Lantian Zheng and Andrew C. Myers. 2007. Dynamic Security Labels and Static Information Flow Control. Intl\u2019 J. of Information Security 6 2\u20133 (March 2007).","DOI":"10.1007\/s10207-007-0019-9"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276485","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3276485","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3276485","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:01:58Z","timestamp":1750208518000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276485"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,24]]},"references-count":40,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2018,10,24]]}},"alternative-id":["10.1145\/3276485"],"URL":"https:\/\/doi.org\/10.1145\/3276485","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2018,10,24]]},"assertion":[{"value":"2018-10-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}