This talk presents a new model for classifying vulnerabilities in computer systems. The model is structurally different than other models. It decomposes vulnerabilities into small parts, called primitive conditions. Our hypothesis is that by examining systems for these conditions, we can detect vulnerabilities. By preventing these conditions from holding, we can prevent vulnerabilities from occurring, even if we do not know that the vulnerability exists. We also present a formal basis for this model. The primitive conditions also enable programs to be tested using a technique called property based testing. This method of testing determines whether a program satisfies a given set of security properties.

Reception following in 301 CSL.