Declassification Policy for Program Complexity Analysis
Article No.: 41, Pages 1 - 14
Abstract
In automated complexity analysis, noninterference-based type systems statically guarantee, via soundness, the property that well-typed programs compute functions of a given complexity class, e.g., the class FP of functions computable in polynomial time. These characterizations are also extensionally complete - they capture all functions - but are not intensionally complete as some polytime algorithms are rejected. This impact on expressive power is an unavoidable cost of achieving a tractable characterization. To circumvent this issue, an avenue arising from security applications is to find a relaxation of noninterference based on a declassification mechanism that allows critical data to be released in a safe and controlled manner. Following this path, we present a new and intuitive declassification policy preserving FP-soundness and capturing strictly more programs than existing noninterference-based systems. We show the versatility of the approach: it also provides a new characterization of the class BFF of second-order polynomial time computable functions in a second-order imperative language, with first-order procedure calls. Type inference is tractable: it can be done in polynomial time.
References
[1]
Michael Backes and Birgit Pfitzmann. 2003. Intransitive non-interference for cryptographic purposes. In SSP 2003. 140--152.
[2]
Patrick Baillot, Ugo Dal Lago, Cynthia Kop, and Deivid Vale. 2024. On Basic Feasible Functionals and the Interpretation Method. In Foundations of Software Science and Computation Structures, FOSSACS 2024 (Lecture Notes in Computer Science, Vol. 14575). Springer, 70--91.
[3]
Stephen Bellantoni and Stephen A. Cook. 1992. A New Recursion-Theoretic Characterization of the Polytime Functions. Comput. Complex. 2 (1992), 97--110.
[4]
Siddharth Bhaskar, Cynthia Kop, and Jakob Grue Simonsen. 2023. Subclasses of Ptime Interpreted by Programming Languages. Theory Comput. Syst. 67, 3 (2023), 437--472.
[5]
Stephen A. Cook. 1992. Computability and complexity of higher type functions. In Logic from Computer Science. Springer, 51--72.
[6]
Stephen A. Cook and Alasdair Urquhart. 1993. Functional interpretations of feasibly constructive arithmetic. Ann. Pure Appl. Logic 63, 2 (1993), 103--200.
[7]
Ugo Dal Lago, Reinhard Kahle, and Isabel Oitavem. 2021. A Recursion-Theoretic Characterization of the Probabilistic Class PP. In Mathematical Foundations of Computer Science (MFCS 2021), Vol. 202. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 35:1--35:12.
[8]
Norman Danner, Jennifer Paykin, and James S. Royer. 2013. A static cost analysis for a higher-order language. In Programming languages meets program verification, PLPV 2013. ACM, 25--34.
[9]
Norman Danner and James S. Royer. 2006. Adventures in time and space. In Principles of Programming Languages, POPL 2006. ACM, 168--179.
[10]
Daniel de Carvalho and Jakob Grue Simonsen. 2014. An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting. In Rewriting and Typed Lambda Calculi (RTA-TLCA 2014) (Lecture Notes in Computer Science, Vol. 8560). Springer, 179--193.
[11]
Jörg Endrullis, Herman Geuvers, Jakob Grue Simonsen, and Hans Zantema. 2011. Levels of undecidability in rewriting. Information and Computation 209, 2 (2011), 227--245.
[12]
Joseph A. Goguen and José Meseguer. 1982. Security policies and security models. In 1982 IEEE Symposium on Security and Privacy. IEEE, 11--11.
[13]
Joseph A. Goguen and José Meseguer. 1984. Unwinding and inference control. In 1984 IEEE Symposium on Security and Privacy. IEEE, 75--75.
[14]
Emmanuel Hainry, Emmanuel Jeandel, Romain Péchoux, and Olivier Zeyen. 2021. ComplexityParser: An Automatic Tool for Certifying Poly-Time Complexity of Java Programs. In Theoretical Aspects of Computing - ICTAC 2021. Springer, 357--365.
[15]
Emmanuel Hainry, Bruce M. Kapron, Jean-Yves Marion, and Romain Péchoux. 2020. A tier-based typed programming language characterizing Feasible Functionals. In Logic in Computer Science, LICS 2020. 535--549.
[16]
Emmanuel Hainry, Bruce M. Kapron, Jean-Yves Marion, and Romain Péchoux. 2022. Complete and tractable machine-independent characterizations of second-order polytime. In Foundations of Software Science and Computation Structures, FOSSACS 2022. 368--388.
[17]
Emmanuel Hainry, Jean-Yves Marion, and Romain Péchoux. 2013. Type-based complexity analysis for fork processes. In Foundations of Software Science and Computation Structures, FOSSACS 2013. Springer, 305--320.
[18]
Emmanuel Hainry and Romain Péchoux. 2018. A type-based complexity analysis of Object Oriented programs. Inf. Comput. 261 (2018), 78--115.
[19]
Emmanuel Hainry and Romain Péchoux. 2020. Theory of higher order interpretations and application to Basic Feasible Functions. Log. Methods Comput. Sci. 16, 4 (2020).
[20]
Emmanuel Hainry and Romain Péchoux. 2023. A General Noninterference Policy for Polynomial Time. In Principles of programming languages, POPL 2023. ACM, 806--832.
[21]
Petr Hájek. 1979. Arithmetical Hierarchy and Complexity of Computation. Theor. Comput. Sci. 8 (1979), 227--237.
[22]
Robert J. Irwin, James S. Royer, and Bruce M. Kapron. 2001. On characterizations of the basic feasible functionals (Part I). J. Funct. Program. 11, 1 (2001), 117--153.
[23]
Neil D. Jones. 2001. The expressive power of higher-order types or, life without CONS. J. Funct. Program. 11, 1 (2001), 5--94.
[24]
Bruce M. Kapron and Stephen A. Cook. 1996. A New Characterization of Type-2 Feasibility. SIAM J. Comput. 25, 1 (1996), 117--132.
[25]
Bruce M. Kapron and Florian Steinberg. 2018. Type-two polynomial-time and restricted lookahead. In Logic in Computer Science, LICS 2018. ACM, 579--588.
[26]
Daniel Leivant. 1991. A foundational delineation of computational feasibility. In Logic in Computer Science (LICS'91). IEEE, 2--3.
[27]
Daniel Leivant and Jean-Yves Marion. 1993. Lambda Calculus Characterizations of Poly-Time. Fundam. Inform. 19, 1/2 (1993), 167--184.
[28]
Peng Li and Steve Zdancewic. 2005. Downgrading policies and relaxed noninterference. In Principles of programming languages, POPL 2005. ACM, 158--170.
[29]
Jean-Yves Marion. 2011. A Type System for Complexity Flow Analysis. In Logic in Computer Science, LICS 2011. IEEE Computer Society, 123--132.
[30]
Andrew C. Myers. 1999. JFlow: practical mostly-static information flow control. In Principles of programming languages, POPL 1999. ACM, 228--241.
[31]
Andrew C. Myers and Barbara Liskov. 2000. Protecting privacy using the decentralized label model. ACM Trans. Softw. Eng. Methodol. 9, 4 (2000), 410--442.
[32]
Andrei Sabelfeld and David Sands. 2009. Declassification: Dimensions and principles. J. Comput. Secur. 17, 5 (oct 2009), 517--548.
[33]
Dennis Volpano, Cynthia Irvine, and Geoffrey Smith. 1996. A sound type system for secure flow analysis. J. Comput. Secur. 4, 2-3 (1996), 167--187.
[34]
Dennis Volpano and Geoffrey Smith. 2000. Verifying secrets and relative secrecy. In Principles of programming languages, POPL 2000. ACM, 268--276.
[35]
Steve Zdancewic and Andrew C. Myers. 2001. Robust declassification. In Computer Security Foundations Workshop, CSFW 2001. IEEE, 15--23.
Index Terms
- Declassification Policy for Program Complexity Analysis
Recommendations
Enforcing robust declassification and qualified robustness
Special issue on CSFW17Noninterference requires that there is no information flow from sensitive to public data in a given system. However, many systems release sensitive information as part of their intended function and therefore violate noninterference. To control ...
End-to-End Enforcement of Erasure and Declassification
CSF '08: Proceedings of the 2008 21st IEEE Computer Security Foundations SymposiumDeclassification occurs when the confidentiality of information is weakened; erasure occurs when the confidentiality of information is strengthened, perhaps to the point of completely removing the information from the system. This paper shows how to ...
Trusted declassification:: high-level policy for a security-typed language
PLAS '06: Proceedings of the 2006 workshop on Programming languages and analysis for securitySecurity-typed languages promise to be a powerful tool with which provably secure software applications may be developed. Programs written in these languages enforce a strong, global policy of noninterferencewhich ensures that high-security data will ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
July 2024
988 pages
ISBN:9798400706608
DOI:10.1145/3661814
- Conference Chair:
- Pawel Sobocinski,
- Program Chairs:
- Ugo Dal Lago,
- Javier Esparza
Copyright © 2024 Copyright is held by the owner/author(s). Publication rights licensed to ACM.
Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of a national government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.
Sponsors
- SIGLOG: ACM Special Interest Group on Logic and Computation
- IEEE Computer Society
In-Cooperation
- EACSL
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 08 July 2024
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- NSERC
Conference
LICS '24
Sponsor:
LICS '24: 39th Annual ACM/IEEE Symposium on Logic in Computer Science
July 8 - 11, 2024
Tallinn, Estonia
Acceptance Rates
LICS '24 Paper Acceptance Rate 72 of 236 submissions, 31%;
Overall Acceptance Rate 215 of 622 submissions, 35%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 35Total Downloads
- Downloads (Last 12 months)35
- Downloads (Last 6 weeks)3
Reflects downloads up to 09 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in