Formally-Based Black-Box Monitoring of Security Protocols
Alfredo Pironti and Jan Jürjens.
In the challenge of getting provably correct implementations of security
protocols, much effort has been recently put into two strategies:
model-driven-development to generate new implementations; and verification of the
source code of already existing implementations. However, no approach currently deals
with legacy implementations for which no source code is available. This paper
presents a formally-based approach to design and implement monitors that stop insecure
protocol runs executed by legacy implementations, without the need of their source
code. We validate the approach at a case study about monitoring several SSL legacy
implementations. Recently, a security bug has been found in the widely deployed
OpenSSL client; our case study shows that our monitor correctly stops the protocol
runs otherwise allowed by the faulty OpenSSL client. Moreover, our monitoring
approach allowed us to detect a new flaw in another open source SSL client
Francesco Gadaleta, Yves Younan and Wouter Joosen.
Reusability of threat models - an experimental evaluation
Per Håkon Meland, Inger Anne Tøndel and Jostein Jensen.
To support software developers in addressing security, we encourage to take advantage of threat models for knowledge sharing and reuse of models to achieve a general increase in efficiency and quality. This paper presents a controlled experiment with a qualitative evaluation of two different methods supporting threat modelling - reuse of categorised misuse case stubs and reuse of full misuse case diagrams. In both methods, misuse case threats were coupled with attack trees to give more insight on the attack techniques and how to mitigate them through security use cases. Seven professional software developers from two European software companies took part in the experiment. Results indicate that reuse improves threat modelling in many ways. Participants were able to identify threats and mitigations they would not have identified otherwise. They also reported that both methods were easy to learn, seemed to improve productivity and that using them were likely to improve their own skills and confidence in results. The methods proved to be rather equal in performance and perception, giving developers the freedom to choose based on personal preference.
Category-based authorisation models: operational semantics and expressive power
Clara Bertolissi and Maribel Fernandez.
In this paper we give an operational specification, using term rewriting, of a category based meta-model of access control. To demonstrate the expressiveness of the meta-model, we show how several traditional access control models, and also some novel models, can be defined as special cases. The operational specification that we give permits declarative representation of access control requirements, is suitable for fast prototyping of access control checking, and facilitates the process of
proving properties of access control policies.
On the Efficient Evaluation of Access Control Constraints
Achim D. Brucker and Helmut Petritsch.
Business requirements for modern enterprise systems usually comprise
a variety of dynamic constraints, i.e., constraints that require a
complex set of context information only available at runtime. Thus,
the efficient evaluation of dynamic constraints, e.g., expressing
separation of duties requirements, becomes an important factor for
the overall performance of the access control enforcement.
Especially in highly distributed systems, e.g., systems based on the
service-oriented architecture paradigm, the time for evaluating
access control constraints depends significantly on the protocol
between the central PDP and the distributed PEP.
In this paper, we present an policy-driven approach for generating
customized protocol for the communication between the PDP and
the PEP. Moreover, we provide a detailed comparison of
several approaches for querying context information during the
evaluation of access control constraints.
Report: Modular safeguards to create holistic security requirement specifications for system of systems
Albin Zuccato, Nils Daniels, Mikael Nilson and Cheevarat Jaampatom.
The specification of security requirements for systems of systems is in practice a fairly constraint activity. It is often performed under time pressure by non-experts in the security field. To overcome these constrains we show how a collection of modular safeguards, which are tailored to the application domain and can therefore be specific but still fairly atomic, are combined into requirement profiles that seamlessly integrates into the overall development approach. The safeguards are grouped into 15 classes which subsume requirements that aim for low, medium and high security capabilities. Each requirement is further specified with a technical description defining actual values. To achieve a holistic coverage, requirement profiles define combinations of the modular safeguards and complete them with organizational safeguards. We show how this approach has developed over the years and present our practical experiences with it.
A Feasibility Study in Model Based Prediction of Impact of Changes on System Quality
Aida Omerovic, Anette Andresen, Håvard Grindheim, Per Myrseth, Atle Refsdal and Ketil Stølen.
We propose a method, called PREDIQT, for model based prediction of impact of architecture design changes on system quality attributes. PREDIQT supports simultaneous analysis of several quality attributes and their trade-offs. This paper argues for the feasibility of the PREDIQT method based on a comprehensive industrial case study targeting a system for managing validation of electronic certicates and signatures worldwide. We first give an overview of the PREDIQT method, and then present an evaluation of the method in terms of a feasibility study and a thought experiment. The evaluation focuses on security and its trade-offs with the overall quality attributes of the target system.
Enforcing consumer-specified security properties for modular software
Giacomo A. Galilei and Vincenzo Gervasi
Nowadays systems that download updates from the net or let the user download third-party code for extending the application functions (plug-ins) are widespread. In these dynamic environments the code that is going to be executed is not known at compile-time, and often not even at application start-up, neither by the application producer nor by the user. This turns reliable, well designed software into a dangerous and potentially malicious software for the user and for the system it runs onto: i.e., a well-behaved modular application becomes the unwilling host for malicious components.
In this scenario, the application producer lines up with the user in requesting that dynamically loaded components must satisfy given security requirements.
In this paper we present a framework the allows the consumer side of untrusted code to state desired properties about it. We exploit the facilities of the so-called virtual execution environments to encode directly into the meta-data of object code a well structured specification.
Once the dynamic component is loaded at run-time by the main application, the framework will recover such specifications and check them against the requirements gathered from the main application, the user and the host operating system, injecting run-time checks as needed into the untrusted code to ensure that the actual behaviour of the component matches the specified one.
Opcode-sequence-based Malware Detection
Igor Santos, Felix Brezo, Javier Nieves, Yoseba Penya, Borja Sanz, Carlos Laorden and Pablo Bringas.
Malware is any malicious code that has the potential to harm any computer or network. The amount of malware is increasing faster every year and poses a serious security threat. Hence, malware detection has become a critical topic in computer security. Currently, signature-based detection is the most extended method within commercial antivirus. Although this method is still used on most popular commercial computer antivirus software, it can only achieve detection once the virus has already caused damage and it is registered. Therefore, it fails to detect new variations of known malware and unknown malware. In this paper, we propose a new method to detect both variants of known malware and unknown malware families. This method is based on the frequency of appearance of opcode sequences. Furthermore, we describe a method to mine the relevance of each opcode and, thereby, weigh each opcode sequence frecuency. We show that this method provides an effective way to detect both variants of known
malware variants and unknown malware.
Formal Verification of Application-Specific Security Properties in a Model-Driven Approach
Nina Moebius, Kurt Stenzel and Wolfgang Reif.
We present a verification method that allows to prove security
for security-critical systems based on cryptographic protocols. Designing
cryptographic protocols is very difficult and error-prone and most
tool-based verification approaches only consider standard security properties
such as secrecy or authenticity. In our opinion, application-specific
security properties give better guarantees. In this paper we illustrate how
to verify properties that are relevant for e-commerce applications, e.g.
’The provider of a copying service does not lose money’. This yields a
more complex security property that is proven using interactive verification.
The verification of this kind of application-specific property is
part of the SecureMDD approach which provides a method to model a
security-critical application with UML and automatically generates executable
code as well as a formal specification for interactive verification
from the UML models.
Automatic Generation of Smart, Security-Aware GUIs
David Basin, Manuel Clavel, Marina Egea and Michael Schläpfer.
In many software applications, users access application data
using graphical user interfaces (GUIs). There is an important, but little
explored, link between visualization and security: when the application
data is protected by an access control policy, the GUI should be aware
of this and respect this policy. For example, the GUI should not display
options to users for actions that they are not authorized to execute on
application data. One step further, the GUI should not, for example,
display options to users for opening other widgets when these widgets
will only display options for actions that the users are not authorized
to execute on application data. That is, the application GUI should not
only be security-aware but also smart. We make this link using a model-
driven development approach. Namely, we define and implement a many-
models-to-model transformation that, given a security-design model and
a GUI model, makes the GUI model both security-aware and smart.
Experiences with PDG-based IFC
Information flow control systems provide the guarantees that are required in today’s security-relevant systems. While the literature has produced a wealth of techniques to ensure a given security policy, there is only a small number of implementations, and even these are mostly restricted to theoretical languages or a subset of an existing language.
Previously, we presented the theoretical foundations and algorithms for dependence-graph-based information flow control (IFC). As a complement, this paper presents the implementation and evaluation of our new approach, the first implementation of a dependence-graph based analysis that accepts full Java bytecode. It shows that the security policy can be annotated in a succinct manner; and the evaluation shows that the increased runtime of our analysis—a result of being flow-, context-, and object-sensitive—is mitigated by better analysis results and elevated practicability. Finally, we show that the scalability of our analysis is not limited by the sheer size of either the security lattice or the dependence graph that represents the program.
Transparent client-side mitigation of malicious cross-domain requests
Philippe De Ryck, Lieven Desmet, Thomas Heyman, Frank Piessens and Wouter Joosen.
Protecting users in the ubiquitous online world is becoming more and
more important, as shown by web application security -- or the lack
thereof -- making the mainstream news. One of the more harmful attacks
is cross-site request forgery (CSRF), which allows an attacker to trick
users into making requests to certain web applications without their
knowledge. Existing client-side protection mechanisms do not fully
mitigate the problem or have a degrading effect on the browsing
experience of the user, especially in an interactive web 2.0
environment. To fill this gap, this paper makes three contributions:
first, a thorough traffic analysis on real-world traffic quantifies the
amount of cross-domain traffic and identifies its specific properties.
Second, a client-side enforcement policy has been constructed to
autonomously mitigate CSRF attacks as precise as possible. This policy
is implemented as a Firefox extension. Third, the granularity of the
policy enforcement is improved even further by incorporating
server-specific policy refinements about possible cross-domain traffic.
Secure Code Generation for Web Applications
Martin Johns, Christian Beyerlein and Joachim Posegga.
A large percentage of recent security problems, such as
Cross-site Scripting or SQL injection, is caused by string-based code
injection vulnerabilities. These vulnerabilities exist because
of implicit code creation through string serialization. Based on an
analysis of the vulnerability class' underlying mechanisms, we
propose a general approach to outfit modern programming languages with
mandatory means for explicit and secure code generation which provide
strict separation between data and code. Using an exemplified
respectively, we show how our approach can be realized and enforced.
On the Use of Grey Box Testing for Revealing SQL Injection-Related Error Message Information Leaks
Ben Smith, Laurie Williams and Andrew Austin.
The complete handling of SQL injection is comprised of two parts: properly protecting the system from malicious input, and preventing any resultant error messages from revealing sensitive information. The goal of this research is to assess the relative effectiveness of white and grey box testing of web applications to reveal both error message information leak and SQL injection vulnerabilities. To produce 100% coverage of 176 SQL statements in four open source web applications, we augmented the original automated white box test cases with grey box tests that use both normal input and 132 forms of malicious input. Although we discovered no SQL injection vulnerabilities, we exposed 17 error message information leak vulnerabilities associated with SQL statements using grey box testing. Our results suggest that security testers that use an iterative, test-driven development process should compose grey box rather than white box tests.
Java vs. PHP: Security Implications of Language Choice for Web Applications
James Walden, Maureen Doyle, Rob Lenhof and John Murray.
While Java and PHP are two of the most popular languages for open source web applications found at freshmeat.net, Java has had a much better security reputation than PHP. In this paper, we examine whether that reputation is deserved. We studied whether the variation in vulnerability density is greater between languages or between different applications written in a single language by comparing eleven open source web applications written in Java with fourteen such applications written in PHP. To compare the languages, we created a Common Vulnerability Density (CVD) metric, which is the count of four vulnerability types common to both languages normalized by code size. We measured CVD for two revisions of each project, one from 2006 and the other from 2008. CVD values were higher for the aggregate PHP code base than the Java code base, but PHP had a better rate of improvement, with a decline from 6.25 to 2.36 vulnerabilities/KLOC compared to 1.15 to 0.63 in Java. These changes arose from an increase in code size in both languages and a decrease in vulnerabilities in PHP. The variation between projects was greater than the variation between languages, ranging from 0.52 to 14.39 for Java and 0.03 to 121.36 in PHP for 2006. We used security and software metrics to examine the sources of difference between projects.
Towards architecture-centric static security analysis of software
Karsten Sohr and Bernhard Berger.
Static security analysis of software has made great progress in the last years. In particular, this applies to the detection of low-level security bugs such as buffer overflows, Cross-Site Scripting and SQL injection vulnerabilities. Complementarily to commercial static code review tools, we present an approach to the static security analysis which is based upon the software architecture using a reverse engineering tool-suite called Bauhaus. This allows one to analyze software on a more abstract level, and a more focused analysis is possible, concentrating on software modules marked as security-critical. In addition, certain security flaws can be detected on the architectural level such as the circumvention of APIs or incomplete enforcement of access control. We discuss our approach in the context of a business application and Android’s Java-based middleware.
Model-driven Security Policy Deployment: Property Oriented Approach
Stere Preda, Nora Cuppens-Boulahia, Frédéric Cuppens, Joaquin Garcia-Alfaro and Laurent Toutain.
We focus in this paper on the issue of formally validating the deployment of access control security policies. Our proposal is the following. First, as input to our approach, we consider a formal expression of the security requirements related to a given system; this ensures the deployment of an anomaly free abstract security policy. Second, we develop the algorithms using a theorem proving approach with a modeling language allowing the specification of the system, of the link between the system and the policy and of certain target security properties. As a result, we obtain a set of proved algorithms that constitute the certified technique for an automatic reliable security policy deployment.