Higher-Order Program Verification and Language-Based Security

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.