INTRODUCTION The objective of this paper is to present a formal approach for the extraction of a simple security models from PHP source code. In paper [1], the issue of identifying statements vulnerable to SQL-injections caused by external input or internal programming was specifically addressed in the static flow analysis perspective of “authorization levels” and “vulnerability” analysis. In this paper, an original approach using formal methods and model checking to address the same vulnerability problem described in [1] is presented. Motivation comes from the relatively greater difficulty to formally prove or reason about the correctness, the complexity, and the performance of the corresponding flow analysis algorithm. Success in the formal modelling and verification strengthens the role privilege analysis approach either solved by flow analysis or by model checking. The objective is to conceive a correspondence between the algorithmic description of the solution method presented in [1] and a temporal logic based formulation of the same problem and perform experimental comparison of results on phpBB application as a case study. II. CONTROL FLOW GRAPH Let CFG = (VCFG, ECFG) be a Control Flow Graph with a unique entry node vin ∈ VCFG and a unique exit node vout ∈ VCFG. Nodes in VCFG can be of type call begin, call end, entry, or exit. Nodes of type generic are involved in intraprocedural control flow; nodes of type call begin, call end, entry, and exit are used in inter-procedural control flow. Edges in ECFG can be of type generic, positive authorization, negative authorization, call, or return. Edges of type generic represent intra-procedural transfers of control that do not change the granted security level; edges of type positive authorization represent intra-procedural transfers of control that change the granted security level to admin level; edges of type negative authorization represent intra-procedural transfers of control that change the granted security level to user level; and edges of type call and return represent inter-procedural control flow links. A. Inter-procedural aspects An edge of type call links a node of type call begin with the entry node of the called procedure. An edge of type return links the exit node of called procedure to the appropriate call end node in the calling procedure.
EXPERIMENTS AND RESULTS The proposed extraction approach has been preliminarily evaluated on a small PHP open source system, phpBB, that implements a bulletin board. Results and execution time performance of the proposed model extraction algorithm are presented and discussed. To evaluate our approach, we have taken a case study perspective about detecting role privilege vulnerabilities. phpBB is a well-known application for its abundance of documented opportunities for security violations in its past versions. Indeed, during the past years and versions, an effort has been made to remove vulnerabilities. For the reported experiments, we have chosen the old version 2.0.0 of phpBB, for which publicly available security bugs have been reported. Our objective is to take an old security flawed version and to automatically detect SQLinjection vulnerabilities both in terms of user data triggered injections and/or possibly malicious code injected by an insider. Syntactic analysis has been achieved by using and extending a Web available JavaCC PHP grammar. Experiments have been performed to evaluate characteristics and performance of the proposed model extraction approach.
DISCUSSION The results obtained from the application of the proposed formal approach on a small PHP application have been compared with those obtained from a previously developed flow analysis approach for the same boolean role privilege analysis problem. Simple boolean security models can be extracted and verified in linear time using the presented algorithms, while general approaches for inter-procedural model checking show a higher computational complexity due to their generality. Results have been sucessfully compared with those previously obtained from the corresponding inter-procedural data-flow vulnerability analysis. There is correspondence between flow analysis and model checking [7], and this study presents some simple anecdotal experience about investigating the same vulnerability problem solved by flow analysis using formal methods and model checking. The authors believe that the formal understanding of security analysis of inter-procedural systems is clearer under the presented model checking perspective than under the previously published flow analysis. Algorithm in Fig. 7 was necessary because some common tools that have been tried for model checking were not able to compute the extracted models. We believe that the number of states and the number of pass variables made their computation explode. For example, Spin model checker executions were often halted by the researchers without reaching the solution, after few days of computation. Identified vulnerabilities are consistent with those produced by flow analysis and are caused by a known error of class “Input Validation” published in phpBB archives [8]. The presented model extraction is largely language independent, at least in the class of imperative languages. Authorization levels in the investigated application are granted by the pattern described in Section II-B. Authorization granting patterns are application dependent and not likely to be reusable across applications. Nevertheless, when security evolution analysis is sought [9], for example to validate successive version of a system, security granting patterns show a certain stability from one version to another.