Peixuan Li
Skip Abstract Section
Abstract
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.
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.
- Alexander Aiken. 1999. Introduction to set constraint-based program analysis. Science of Computer Programming 35, 2-3 (1999), 79–111. Google Scholar
Digital Library
- Alexander Aiken, Edward L Wimmers, and TK Lakshman. 1994. Soft typing with conditional types. In Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, 163–173. Google ScholarDigital Library
- Owen Arden, Michael D. George, Jed Liu, K. Vikram, Aslan Askarov, and Andrew C. Myers. 2012. Sharing Mobile Code Securely With Information Flow Control. In Proc. IEEE Symp. on Security and Privacy (S&P). 191–205. Google ScholarDigital Library
- Lennart Augustsson. 1998. Cayenne—a language with dependent types. In Proc. 3 rd ACM SIGPLAN Int’l Conf. on Functional Programming (ICFP). 239–250. Google ScholarDigital Library
- D Elliott Bell and Leonard J LaPadula. 1973. Secure Computer Systems: mathematical foundations and model. Technical Report M74-244. MITRE Corp., Bedford, MA.Google Scholar
- Hongxu Chen, Alwen Tiu, Zhiwu Xu, and Yang Liu. 2018. A permission-dependent type system for secure information flow analysis. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF). IEEE, 218–232.Google ScholarCross Ref
- Juan Chen, Ravi Chugh, and Nikhil Swamy. 2010. Type-preserving Compilation of End-to-end Verification of Security Enforcement. In Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI). 412–423. Google ScholarDigital Library
- Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George C. Necula. 2007. Dependent types for low-level programming. In Proc. European Symposium on Programming (ESOP). 520–535. Google ScholarDigital Library
- Jeffrey S Fenton. 1974. Memoryless subsystems. Comput. J. 17, 2 (1974), 143–147.Google ScholarCross Ref
- Andrew Ferraiuolo, Rui Xu, Danfeng Zhang, Andrew C. Myers, and G. Edward Suh. 2017. Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis. In Proc. Int’l Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS). 555–568. Google ScholarDigital Library
- Joseph A. Goguen and Jose Meseguer. 1982. Security Policies and Security Models. In Proc. IEEE Symp. on Security and Privacy (S&P). 11–20.Google Scholar
- Robert Grabowski and Lennart Beringer. 2009. Noninterference with Dynamic Security Domains and Policies. In Advances in Computer Science – ASIAN 2009. Information Security and Privacy. 54–68. LNCS 5913. Google ScholarDigital Library
- Sebastian Hunt and David Sands. 2006. On Flow-sensitive Security Types. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’06). ACM, New York, NY, USA, 79–90. Google ScholarDigital Library
- Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, and Steve Zdancewic. 2008. AURA: A Programming Language for Authorization and Audit. In Proc. 13 th ACM SIGPLAN Int’l Conf. on Functional Programming (ICFP). 27–38. Google ScholarDigital Library
- Gurvan Le Guernic and Thomas Jensen. 2005. Monitoring Information Flow. In Workshop on Foundations of Computer Security - FCS’05. 19–30.Google Scholar
- Peixuan Li and Danfeng Zhang. 2017. Towards a Flow- and Path-Sensitive Information Flow Analysis. In Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF). 53–67.Google ScholarCross Ref
- Jed Liu, Michael D. George, K. Vikram, Xin Qi, Lucas Waye, and Andrew C. Myers. 2009. Fabric: A Platform For Secure Distributed Computation and Storage. In Symp. on Operating Systems Principles (SOSP). 321–334. Google ScholarDigital Library
- Luísa Lourenço and Luís Caires. 2015. Dependent Information Flow Types. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 317–328. Google ScholarDigital Library
- Per Martin-Löf. 1982. Constructive mathematics and computer programming. Studies in Logic and the Foundations of Mathematics 104 (1982), 153–175.Google ScholarCross Ref
- Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Proc. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Google ScholarDigital Library
- Toby Murray, Robert Sison, Edward Pierzchalski, and Christine Rizkallah. 2016. Compositional verification and refinement of concurrent value-dependent noninterference. In Computer Security Foundations Symposium (CSF), 2016 IEEE 29th. IEEE, 417–431.Google ScholarCross Ref
- Andrew C. Myers. 1999. JFlow: Practical Mostly-Static Information Flow Control. In Proc. 26 th ACM Symposium on Principles of Programming Languages (POPL). 228–241. http://www.cs.cornell.edu/andru/papers/popl99/popl99.pdf Google ScholarDigital Library
- 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 .Google Scholar
- 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 .Google Scholar
- 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).Google Scholar
- François Pottier and Vincent Simonet. 2002. Information flow inference for ML. In Proc. 29 th ACM Symposium on Principles of Programming Languages (POPL). 319–330. Google ScholarDigital Library
- Jakob Rehof et al. 1999. Tractable constraints in finite semilattices. Science of Computer Programming 35, 2-3 (1999), 191–221. Google ScholarDigital Library
- Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. 2008. Liquid Types. In Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI). 159–169. Google ScholarDigital Library
- Andrei Sabelfeld and Alejandro Russo. 2010. From dynamic to static and back: Riding the roller coaster of information-flow control research. Perspectives of Systems Informatics (2010), 352–365. Google ScholarDigital Library
- Paritosh Shroff, Scott Smith, and Mark Thober. 2007. Dynamic dependency monitoring to secure information flow. In Computer Security Foundations Symposium, 2007. CSF’07. 20th IEEE. IEEE, 203–217. Google ScholarDigital Library
- Vincent Simonet. 2003. The Flow Caml System: documentation and user’s manual. Technical Report 0282. Institut National de Recherche en Informatique et en Automatique (INRIA).Google Scholar
- Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. 2011. Secure Distributed Programming with Value-dependent Types. In Proc. 16 th ACM SIGPLAN Int’l Conf. on Functional Programming (ICFP). 266–278. Google ScholarDigital Library
- Nikhil Swamy, Brian J. Corcoran, and Michael Hicks. 2008. Fable: A Language for Enforcing User-defined Security Policies. In Proc. IEEE Symp. on Security and Privacy (S&P). 369–383. Google ScholarDigital Library
- Stephen Tse and Steve Zdancewic. 2007. Run-Time Principals in Information-Flow Type Systems. ACM Trans. on Programming Languages and Systems 30, 1 (2007), 6. Google ScholarDigital Library
- Jeffrey A Vaughan and Stephen Chong. 2011. Inference of expressive declassification policies. In Security and Privacy (SP), 2011 IEEE Symposium on. IEEE, 180–195. Google ScholarDigital Library
- Niki Vazou, Eric L Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014. Refinement types for Haskell. In ACM SIGPLAN Notices, Vol. 49. ACM, 269–282. Google ScholarDigital Library
- Dennis Volpano, Geoffrey Smith, and Cynthia Irvine. 1996. A Sound Type System for Secure Flow Analysis. Journal of Computer Security 4, 3 (1996), 167–187. Google ScholarDigital Library
- Hongwei Xi. 2000. Imperative programming with dependent types. In Proc. IEEE Symposium on Logic in Computer Science. 375–387. Google ScholarDigital Library
- Hongwei Xi and Frank Pfenning. 1999. Dependent Types in Practical Programming. In Proc. ACM Symp. on Principles of Programming Languages (POPL). 214–227. Google ScholarDigital Library
- Danfeng Zhang and Andrew C. Myers. 2014. Toward General Diagnosis of Static Errors. In Proc. 14 th ACM Symposium on Principles of Programming Languages (POPL). 569–581. http://www.cs.cornell.edu/andru/papers/diagnostic Google ScholarDigital Library
- Danfeng Zhang, Yao Wang, G. Edward Suh, and Andrew C. Myers. 2015. A Hardware Design Language for Timing-Sensitive Information-Flow Security. In Proc. 20 th Int’l Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS). 503–516. Google ScholarDigital Library
- Lantian Zheng and Andrew C. Myers. 2007. Dynamic Security Labels and Static Information Flow Control. Intl’ J. of Information Security 6, 2–3 (March 2007). Google ScholarDigital Library
Index Terms
- A derivation framework for dependent security label inference
Recommendations
Transductive Multilabel Learning via Label Set Propagation
The problem of multilabel classification has attracted great interest in the last decade, where each instance can be assigned with a set of multiple class labels simultaneously. It has a wide variety of real-world applications, e.g., automatic image ...
Learning Label-Specific Features and Class-Dependent Labels for Multi-Label Classification
Binary Relevance is a well-known framework for multi-label classification, which considers each class label as a binary classification problem. Many existing multi-label algorithms are constructed within this framework, and utilize identical data ...
Semi-supervised multi-label classification using incomplete label information
Highlights- An inductive semi-supervised method called Smile is proposed for multi-label classification using incomplete label information.
AbstractClassifying multi-label instances using incompletely labeled instances is one of the fundamental tasks in multi-label learning. Most existing methods regard this task as supervised weak-label learning problem and assume sufficient ...
Comments