 |
    |
Verification of CERT Secure Coding Rules: Case Studies
Syrine Tlili, XiaoChun Yang, Rachid Hadjidj, and Mourad Debbabi*
Computer Security Laboratory, Concordia Institute for Information Systems Engineering, Concordia University, Montreal (QC), Canadas_tlili@ciise.concordia.ca
xc_yang@ciise.concordia.ca
hadjidj@ciise.concordia.ca
debbabi@ciise.concordia.ca
Abstract. Growing security requirements for systems and applications have raised the stakes on software security verification techniques. Recently, model-checking is settling in the arena of software verification. It is effective in verifying high-level security properties related to software functionalities. In this paper, we present the experiments conducted with our security verification framework based on model-checking. We embedded a wide range of the CERT secure coding rules into our framework. Then, we verified real software packages against these rules for purpose of demonstrating the capability and the efficiency of our tool in detecting real errors.
*This research is the result of a fruitful collaboration between CSL (Computer Security Laboratory) of Concordia University, DRDC (Defence Research and Development Canada) Valcartier and Bell Canada under the NSERC DND Research Partnership Program.
LNCS 5871, p. 913 ff.
lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2009