Engineering Secure Software and Systems

The verification of access controls is essential for providing secure systems. Model checking is an automated technique used for verifying finite state machines. The properties to be verified are usually expressed as formula in temporal logic. In this paper we present an approach to verify access control security properties of a security annotated business process model. To this end we utilise a security enhanced BPMN notation to define access control properties.

To enhance the usability the complex and technical details are hidden from the process modeller by using an automatic translation of the process model into a process meta language (Promela) based on Coloured Petri net (CPN) semantics.

The model checker SPIN is used for the process model verification and a trace file is written to provide visual feedback to the modeller on the abstraction level of the verified process model. As a proof of concept the described translation methodology is implemented as a plug-in for the free web-based BPMN modelling tool Oryx.

We present an approach that addresses both formal specification and verification as well as runtime enforcement of RBAC access control policies including application specific constraints such as separation of duties (SoD). We introduce Temporal \(\cal{Z}\), a formal language based on Z and temporal logic, which provides domain specific predicates for expressing RBAC and SoD constraints. An aspect-oriented language with domain specific concepts for RBAC and SoD constraints is used for the runtime enforcement of policies. Enforcement aspects are automatically generated from Temporal \(\cal{Z}\) specifications hence avoiding the possibility of errors and inconsistencies that may be introduced when enforcement code is written manually. Furthermore, the use of aspects ensures the modularity of the enforcement code and its separation from the business logic.

Through first-responder access to sensitive information for which they have not been pre-vetted, lives and property can be saved. We describe enhancements to a trusted emergency information management (EIM) system that securely allows for extraordinary access to sensitive information during a crisis. A major component of the architecture is the end-user device, the security of which is enhanced with processor-level encryption of memory. This paper introduces an approach to more efficiently use the processor-encryption feature for secure data storage, as well as ISA instructions for the management of emergency state.

We present an approach to security requirements engineering, which makes use of special kinds of problem frames that serve to structure, characterize, analyze, and solve software development problems in the area of software and system security.

In this paper, we focus on confidentiality problems. We enhance previously published work by formal behavioral frame descriptions, which enable software engineers to unambiguously specify security requirements. Consequently, software engineers can prove that the envisaged solutions provide functional correctness and that the solutions fulfill the specified security requirements.

This paper deals with architectural designs that specify components of a system and the permitted flows of information between them. In the process of systems development, one might refine such a design by viewing a component as being composed of subcomponents, and specifying permitted flows of information between these subcomponents and others in the design. The paper studies the soundness of such refinements with respect to a spectrum of different semantics for information flow policies. These include Goguen and Meseguer’s purge-based definition, Haigh and Young’s intransitive purge-based definition, and some more recent notions TA-security, TO-security and ITO-security defined by van der Meyden. It is also shown that refinement preserves weak access control structure, an implementation mechanism that ensures TA-security.

Injection attacks and their defense require a lot of creativity from attackers and secure system developers. Unfortunately, as attackers rely increasingly on systematic approaches to find and exploit a vulnerability, developers follow the traditional way of writing ad hoc checks in source code. This paper shows that security engineering to prevent injection attacks need not be ad hoc. It shows that protection can be introduced at different layers of a system by systematically applying general purpose security-oriented program transformations. These program transformations are automated so that they can be applied to new systems at design and implementation stages, and to existing ones during maintenance.

Software vendors are increasingly concerned about mitigating the security risk of their software. Code quality improvement is a traditional approach to mitigate security risk; measuring and reducing the attack surface of software is a complementary approach. In this paper, we apply a method for measuring attack surfaces to enterprise software written in Java. We implement a tool as an Eclipse plugin to measure an SAP software system’s attack surface in an automated manner. We demonstrate the feasibility of our approach by measuring the attack surfaces of three versions of an SAP software system. We envision our measurement method and tool to be useful to software developers for improving software security and quality.

When a vulnerability is discovered in a cryptographic algorithm, or in a specific implementation of that algorithm, it is important that software using that algorithm or implementation is upgraded quickly. Hence, modern cryptographic libraries such as the .NET crypto libraries are designed to be extensible with new algorithms. In addition, they also support algorithm and implementation independent use. Software written against these libraries can be implemented such that switching to a new crypto algorithm or implementation requires very little effort.

This paper reports on our experiences with the implementation of a number of extensions to the .NET cryptographic framework. The extensions we consider are smart card based implementations of existing algorithms. We evaluate the extensibility of the libraries, and the support for implementation independence. We identify several problems with the libraries that have a negative impact on these properties, and we propose solutions.

The main conclusion of the paper is that extensibility and implementation independence can be substantially improved with only minor changes. These changes maintain backwards compatibility for client code.

Discovery of security vulnerabilities is on the rise. As a result, software development teams must place a higher priority on preventing the injection of vulnerabilities in software as it is developed. Because the focus on software security has increased only recently, software development teams often do not have expertise in techniques for identifying security risk, understanding the impact of a vulnerability, or knowing the best mitigation strategy. We propose the Protection Poker activity as a collaborative and informal form of misuse case development and threat modeling that plays off the diversity of knowledge and perspective of the participants. An excellent outcome of Protection Poker is that security knowledge passed around the team. Students in an advanced undergraduate software engineering course at North Carolina State University participated in a Protection Poker session conducted as a laboratory exercise. Students actively shared misuse cases, threat models, and their limited software security expertise as they discussed vulnerabilities in their course project. We observed students relating vulnerabilities to the business impacts of the system. Protection Poker lead to a more effective software security learning experience than in prior semesters. A pilot of the use of Protection Poker with an industrial partner began in October 2008. The first security discussion structured via Protection Poker caused two requirements to be revised for added security fortification; led to the immediate identification of one vulnerability in the system; initiated a meeting on the prioritization of security defects; and instigated a call for an education session on preventing cross site scripting vulnerabilities.

In the search for metrics that can predict the presence of vulnerabilities early in the software life cycle, there may be some benefit to choosing metrics from the non-security realm. We analyzed non-security and security failure data reported for the year 2007 of a Cisco software system. We used non-security failure reports as input variables into a classification and regression tree (CART) model to determine the probability that a component will have at least one vulnerability. Using CART, we ranked all of the system components in descending order of their probabilities and found that 57% of the vulnerable components were in the top nine percent of the total component ranking, but with a 48% false positive rate. The results indicate that non-security failures can be used as one of the input variables for security-related prediction models.

Attack graphs are valuable vulnerabilities analysis tools to network defenders and may be classified to two kinds by application. One is the partial attack graphs which illustrate the potential interrelations among the known vulnerabilities just related to the given attack goal in the targeted network, the other is full attack graphs which evaluate the potential interrelations among all the known vulnerabilities in the targeted network. The previous approaches to generating full attack graphs are suffering from two issues. One is the effective modeling language for full attack graphs generation and the other is the scalability to large enterprise network. In this paper, we firstly present a novel conceptual model for full attack graph generation that introduces attack pattern simplifying the process of modeling the attacker. Secondly, a formal modeling language VAML is proposed to describe the various elements in the conceptual model. Thirdly, based on VAML, a scalable approach to generate full attack graphs is put forward. The prototype system CAVS has been tested on an operational network with over 150 hosts. We have explored the system’s scalability by evaluating simulated networks with up to one thousand hosts and various topologies. The experimental result shows the approach could be applied to large networks.

Memory errors continue to be a major source of software failure. To address this issue, we present MEDS (Memory Error Detection System), a system for detecting memory errors within binary executables. The system can detect buffer overflow, uninitialized data reads, double-free, and deallocated memory access errors and vulnerabilities. It works by using static analysis to prove memory accesses safe. If a memory access cannot be proven safe, MEDS falls back to run-time analysis. The system exceeds previous work with dramatic reductions in false positives, as well as covering all memory segments (stack, static, heap).

With the increasingly important role of web applications in online services and business systems, vulnerabilities such as SQL Injection have become serious security threats. Finding these vulnerabilities by manual testing is a time-consuming and error-prone practice that may result in some potential vulnerabilities being missed due to some execution branches being missed. In this paper, we describe an automatic security testing method to find vulnerabilities in web applications; this method utilizes test data generation techniques for improving the code coverage. Our security testing involves automatic attack request generation and automatic security checking using dynamic tainting technique that detects dangerous contents originating from untrustworthy sources in commands and outputs. Automatic constraint-based test data generation helps to create test data for executing program branches that may have remained unexecuted in previous tests. The experimental results indicate that our method is effective to find new vulnerabilities, and test data generation may help to improve the effectiveness of detection.

To offer successful products and services in the telecom business requires to show that the specified security is implemented as expected. Functional security testing is suitable for this purpose as it bridges the gap between software and security testing. In this paper we describe the aspects of such a functional security testing approach. Further we provide evidence for a practical application of our approach and show the benefits we found.

To understand the effect of code complexity on static analysis, thirty-five format string vulnerabilities were studied. We analyzed two code samples for each vulnerability, one containing the vulnerability and one in which the vulnerability was fixed. We examined the effect of code complexity on the quality of static analysis results, including successful detection and false positive rates. Static analysis detected 63% of the format string vulnerabilities, with detection rates decreasing with increasing code complexity. When the tool failed to detect a bug, it was for one of two reasons: the absence of security rules specifying the vulnerable function or the presence of a bug in the static analysis tool. Complex code is more likely to contain complicated code constructs and obscure format string functions, resulting in lower detection rates.