| Introduction | p. 1 |
| Context and motivation | p. 1 |
| Software certification | p. 4 |
| Certification vs. standardization | p. 5 |
| Certification authorities | p. 5 |
| Software security certification | p. 6 |
| The state of the art | p. 8 |
| Changing scenarios | p. 9 |
| Certifying Open source | p. 9 |
| Conclusions | p. 12 |
| References | p. 12 |
| Basic Notions on Access Control | p. 15 |
| Introduction | p. 15 |
| Access Control | p. 17 |
| Discretionary Access Control | p. 18 |
| Mandatory Access Control | p. 19 |
| Role Based Access Control | p. 24 |
| Conclusions | p. 24 |
| References | p. 25 |
| Test based security certifications | p. 27 |
| Basic Notions on Software Testing | p. 27 |
| Types of Software Testing | p. 30 |
| Automation of Test Activities | p. 34 |
| Fault Terminology | p. 34 |
| Test Coverage | p. 36 |
| Test-based Security Certification | p. 37 |
| The Trusted Computer System Evaluation Criteria (TCSEC) standard | p. 39 |
| CTCPEC | p. 46 |
| ITSEC | p. 46 |
| The Common Criteria: A General Model for Test-based Certification | p. 47 |
| CC components | p. 48 |
| Conclusions | p. 59 |
| References | p. 60 |
| Formal methods for software verification | p. 63 |
| Introduction | p. 63 |
| Formal methods for software verification | p. 65 |
| Model Checking | p. 65 |
| Static Analysis | p. 69 |
| Untrusted code | p. 73 |
| Security by contract | p. 74 |
| Formal Methods for Error Detection in OS C-based Software | p. 75 |
| Static Analysis for C code verification | p. 76 |
| Model Checking for large-scale C-based Software verification | p. 81 |
| Symbolic approximation for large-scale OS software verification | p. 83 |
| Conclusion | p. 86 |
| References | p. 86 |
| OSS security certification | p. 89 |
| Open source software (OSS) | p. 89 |
| Open Source Licenses | p. 90 |
| Specificities of Open Source Development | p. 93 |
| OSS security | p. 97 |
| OSS certification | p. 99 |
| State of the art | p. 100 |
| Security driven OSS development | p. 104 |
| Security driven OSS development: A case study on Single Sign-On | p. 105 |
| Single Sign-On: Basic Concepts | p. 105 |
| A ST-based definition of trust models and requirements for SSO solutions | p. 107 |
| Requirements | p. 116 |
| A case study: CAS++ | p. 118 |
| Conclusions | p. 121 |
| References | p. 122 |
| Case Study 1: Linux certification | p. 125 |
| The Controlled Access Protection Profile and the SLES8 Security Target | p. 125 |
| SLES8 Overview | p. 126 |
| Target of Evaluation (TOE) | p. 127 |
| Security environment | p. 128 |
| Security objectives | p. 129 |
| Security requirements | p. 130 |
| Evaluation process | p. 132 |
| Producing the Evidence | p. 133 |
| The Linux Test Project | p. 134 |
| Writing a LTP test case | p. 135 |
| Evaluation Tests | p. 141 |
| Running the LTP test suite | p. 141 |
| Test suite mapping | p. 142 |
| Automatic Test Selection Example Based on SLES8 Security Functions | p. 146 |
| Evaluation Results | p. 148 |
| Horizontal and Vertical reuse of SLES8 evaluation | p. 149 |
| Across distribution extension | p. 149 |
| SLES8 certification within a composite product | p. 151 |
| Conclusions | p. 153 |
| References | p. 153 |
| Case Study 2: ICSA and CCHIT Certifications | p. 155 |
| Introduction | p. 155 |
| ICSA Dynamic Certification Framework | p. 157 |
| A closer look to ICSA certification | p. 158 |
| Certification process | p. 158 |
| A case study: the ICSA certification of the Endian firewall | p. 159 |
| Endian Test Plan | p. 161 |
| Hardware configuration | p. 161 |
| Software configuration | p. 161 |
| Features to test | p. 161 |
| Testing tools | p. 163 |
| Testing | p. 164 |
| Configuration | p. 164 |
| Logging | p. 165 |
| Administration | p. 166 |
| Security testing | p. 166 |
| The CCHIT certification | p. 168 |
| The CCHIT certification process | p. 170 |
| Conclusions | p. 170 |
| References | p. 171 |
| The role of virtual testing labs | p. 173 |
| Introduction | p. 173 |
| An Overview of Virtualization Internals | p. 176 |
| Virtualization Environments | p. 177 |
| Comparing technologies | p. 179 |
| Virtual Testing Labs | p. 180 |
| The Open Virtual Testing Lab | p. 180 |
| Xen Overview | p. 181 |
| OVL key aspects | p. 181 |
| Hardware and Software Requirements | p. 182 |
| OVL Administration Interface | p. 184 |
| Using OVL to perform LTP tests | p. 184 |
| Conclusions | p. 186 |
| References | p. 186 |
| Long-term OSS security certifications: An Outlook | p. 187 |
| Introduction | p. 187 |
| Long-term Certifications | p. 189 |
| Long-lived systems | p. 189 |
| Long-term certificates | p. 190 |
| On-demand certificate checking | p. 192 |
| The certificate composition problem | p. 194 |
| Conclusions | p. 195 |
| References | p. 196 |
| An example of a grep-based search/match phase | p. 199 |
| Index | p. 201 |
| Table of Contents provided by Ingram. All Rights Reserved. |
