Abstract
Language-based security has been a hot research area of computer security in the last decade. It addresses various concerns about software security by using programming language techniques such as type systems and program analysis/transformation. Thus, advance in programming language research can also benefit language-based security. This paper reports some recent advance in verification techniques for higher-order programs, and discusses its applications to language-based security. More specifically, we summarize the recent result on model-checking of higher-order recursion schemes, and show how it may be applied to language-based security such as secure information flow and stack-based access control.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS 2006, pp. 81–90. IEEE Computer Society Press, Los Alamitos (2006)
Knapik, T., Niwinski, D., Urzyczyn, P.: Higher-order pushdown trees are easy. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 205–222. Springer, Heidelberg (2002)
Igarashi, A., Kobayashi, N.: Resource usage analysis. ACM Transactions on Programming Languages and Systems 27(2), 264–313 (2005)
Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pp. 416–428 (2009)
Kobayashi, N.: Model-checking higher-order functions. In: Proceedings of PPDP 2009 (to appear 2009)
Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. Preprint (2009)
Kobayashi, N., Ong, C.H.L.: Complexity of model checking recursion schemes for fragments of the modal mu-calculus. In: Proceedings of ICALP 2009. LNCS. Springer, Heidelberg (2009)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Selected Areas in Communications 21(1), 5–19 (2003)
Loader, R.: Finitary pcf is not decidable. Theoretical Computer Science 266(1-2), 341–364 (2001)
Lindholm, T., Yellin, F.: The Java Virtual Machine Specification, 2nd edn. Addison Wesley, Reading (1999)
Pottier, F., Skalka, C., Smith, S.F.: A systematic approach to static access control. ACM Transactions on Programming Languages and Systems 27(2), 344–382 (2005)
Fournet, C., Gordon, A.D.: Stack inspection: Theory and variants. ACM Transactions on Programming Languages and Systems 25(3), 360–399 (2003)
Abadi, M., Fournet, C.: Access control based on execution history. In: Proceedings of the Network and Distributed System Security Symposium (NDSS 2003). The Internet Society, San Diego (2003)
Wang, J., Takata, Y., Seki, H.: HBAC: A model for history-based access control and its model checking. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 263–278. Springer, Heidelberg (2006)
Necula, G.C.: Proof-carrying code. In: Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pp. 106–119 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kobayashi, N. (2009). Higher-Order Program Verification and Language-Based Security. In: Datta, A. (eds) Advances in Computer Science - ASIAN 2009. Information Security and Privacy. ASIAN 2009. Lecture Notes in Computer Science, vol 5913. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10622-4_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-10622-4_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-10621-7
Online ISBN: 978-3-642-10622-4
eBook Packages: Computer ScienceComputer Science (R0)