Sicherheitsseminar 2011
Aus PPWiki
Sicherheitsseminar 2011
Achtung: Die verlinkten PDF Dateien sind nur aus dem Uni-Netz erreichbar. Verwenden Sie ggf. den VPN-Client des KIT.
Bekannte, wichtige und neue Projekte auf dem Gebiet
RS3: Reliably Secure Software Systems. DFG gesponsortes SchwerPunkt Programm (SPP)
Homepage: [www.reliably-secure-software-systems.de]
Brandaktuell! Startete Oktober 2010 und läuft 6 Jahre. Rege Beteiligung (3 von 14 Projekten) unserer Fakultät:
- DeduSec: Program-level Specification and Deductive Verification of Security Properties, Prof. Dr. Bernhard Beckert, Prof. Dr. Peter H. Schmitt, Karlsruhe Institute of Technology
- IFC for Mobile Components: Information Flow Control for Mobile Components Based on Precise Analysis for Parallel Programs, Prof. Dr. Markus Müller-Olm, WWU Münster, Prof. Dr.-Ing. Gregor Snelting, Karlsruhe Institute of Technology
- System-wide data-driven runtime usage control across layers of abstraction, Prof. Dr. Alexander Pretschner, Karlsruhe Institute of Technology
Mobius: Mobility, Ubiquity and Security. EU gesponsortes Grossprojekt
Handyapplikationen mit integrierten Sicherheitsbeweisen.
Homepage: [mobius.inria.fr]
Startete September 2005 und lief für 4 Jahre.
Interessante Konferenzen
- Sicherheit
- JIS: International Journal of Information Security
- JCS: Journal of Computer Security
- ESORICS: European Symposium on Research in Computer Security
- ESSoS: International Symposium on Engineering Secure Software and Systems
- SEC: International Information Security Conference
- CSF: Computer Security Foundations Symposium/Workshop
- ICISS: International Conference on Information Systems Security
- FAST: International Workshop on Formal Aspects of Security & Trust
- SSP: IEEE Symposium on Security and Privacy
- Sicherheit, Programmanalyse & Programmiersprachen
- PLAS: Workshop on Programming Languages and Analysis for Security
- Programmanalyse, Programmiersprachen
- TOPLAS: Transactions on Programming Languages and Systems
- PLDI: Programming Language Design and Implementation
- POPL: Principles of Programming Languages
- ISSTA: International Symposium on Software Testing and Analysis
- SCAM: International Working Conference on Source Code Analysis and Manipulation
Themen
IFC mit Typsystemen
- Andrew C. Myers: JFlow: practical mostly-static information flow control, POPL 1999 [PDF]
- Thema
- Information Flow Control durch Quellcodeanalyse von erweitertem Javacode. Zusätzlich auf der Homepage von [Jif] nachsehen, was die neuen Änderungen im Vergleich zu JFlow sind.
- Abstract
- A promising technique for protecting privacy and integrity of sensitive data is to statically check information flow within programs that manipulate the data. While previous work has proposed programming language extensions to allow this static checking, the resulting languages are too restrictive for practical use and have not been implemented. In this paper, we describe the new language JFlow, an extension to the Java language that adds statically-checked information flow annotations. JFlow provides several new features that make information flow checking more flexible and convenient than in previous models: a decentralized label model, label polymorphism, run-time label checking, and automatic label inference. JFlow also supports many language features that have never been integrated successfully with static information flow control, including objects, subclassing, dynamic type tests, access control, and exceptions. This paper defines the JFlow language and presents formal rules that are used to check JFlow programs for correctness. Because most checking is static, there is little code space, data space, or run-time overhead in the JFlow implementation.
- Dennis Volpano, Geoffrey Smith, Cynthia Irvine: A sound type system for secure flow analysis, JCS 1996 [PDF]
- Thema
- Grundlagen: Information Flow Control durch Sprachdesign mit Typsystemen
- Abstract
- Ensuring secure information flow within programs in the context of multiple sensitivity levels has been widely studied. Especially noteworthy is Denning’s work in secure flow analysis and the lattice model. Until now, however, the soundness of Denning’s analysis has not been established satisfactorily. We formulate Denning’s approach as a type system and present a notion of soundness for the system that can be viewed as a form of noninterference. Soundness is established by proving, with respect to a standard programming language semantics, that all well-typed programs have this noninterference property.
IFC mit Abhängigkeitsgraphen
- Christian Hammer, Gregor Snelting: Flow-Sensitive, Context-Sensitive, and Object-sensitive Information Flow Control Based on Program Dependence Graphs, IJIS 2009 [PDF]
- Thema
- IFC für Java-Programme mit Abhängigkeitsgraphen.
- Abstract
- Information flow control (IFC) checks whether a program can leak secret data to public ports, or whether critical computations can be influenced from outside. But many IFC analyses are imprecise, as they are flow-insensitive, context-insensitive, or object-insensitive; resulting in false alarms.
- We argue that IFC must better exploit modern program analysis technology, and present an approach based on program dependence graphs (PDG). PDGs have been developed over the last 20 years as a standard device to represent information flow in a program, and today can handle realistic programs. In particular, our dependence graph generator for full Java bytecode is used as the basis for an IFC implementation which is more precise and needs less annotations than traditional approaches.
- We explain PDGs for sequential and multi-threaded programs, and explain precision gains due to flow-, context-, and object-sensitivity. We then augment PDGs with a lattice of security levels and introduce the flow equations for IFC. We describe algorithms for flow computation in detail and prove their correctness. We then extend flow equations to handle declassification, and prove that our algorithm respects monotonicity of release. Finally, examples demonstrate that our implementation can check realistic sequential programs in full Java bytecode.
- Thomas Reps, Susan Horwitz, Mooly Sagiv, Genevieve Rosay: Speeding up Slicing, FSE 1994 [PDF]
- Thema
- Grundlagen von Systemabhängigkeitsgraphen und Slicing.
- Abstract
- Program slicing is a fundamental operation for many software engineering tools. Currently, the most efficient algorithm for interprocedural slicing is one that uses a program representation called the system dependence graph. This paper defines a new algorithm for slicing with system dependence graphs that is asymptotically faster than the previous one. A preliminary experimental study indicates that the new algorithm is also significantly faster in practice, providing roughly a 6-fold speedup on examples of 348 to 757 lines.
- Jeanne Ferrante, Karl J. Ottenstein, Joe D. Warren: The program dependence graph and its use in optimization, TOPLAS 1987 [PDF]
- Thema
- Grundlagen von Abhängigkeitsgraphen.
- Abstract
- In this paper we present an intermediate program representation, called the program dependence graph (PDG), that makes explicit both the data and control dependences for each operation in a program. Data dependences have been used to represent only the relevant data flow relationships of a program. Control dependences are introduced to analogously represent only the essential control flow relationships of a program. Control dependences are derived from the usual control flow graph. Many traditional optimizations operate more efficiently on the PDG. Since dependences in the PDG connect computationally related parts of the program, a single walk of these dependences is sufficient to perform many optimizations. The PDG allows transformations such as vectorization, that previously required special treatment of control dependence, to be performed in a manner that is uniform for both control and data dependences. Program transformations that require interaction of the two dependence types can also be easily handled with our representation. As an example, an incremental approach to modifying data dependences resulting from branch deletion or loop unrolling is introduced. The PDG supports incremental optimization, permitting transformations to be triggered by one another and applied only to affected dependences.
Nichtinterferenz und Deklassifikation
- Heiko Mantel, Alexander Reinhard: Controlling the what and where of declassification in language-based security, ESOP 2007 [PDF]
- Thema
- Regeln fuer sinnvolle Deklassifikation
- Abstract
- While a rigorous information flow analysis is a key step in obtaining meaningful end-to-end confidentiality guarantees, one must also permit possibilities for declassification. Sabelfeld and Sands categorized the existing approaches to controlling declassification in their overview along four dimensions and according to four prudent principles [16].
- In this article, we propose three novel security conditions for controlling the dimensions where and what, and we explain why these conditions constitute improvements over prior approaches. Moreover, we present a type-based security analysis and, as another novelty, prove a soundness result that considers more than one dimension of declassification.
- Andrei Sabelfeld, David Sands: Dimensions and Principles of Declassification,, IEEE Computer Security Foundations Workshop 2005 [PDF] oder Journal Artikel JCS 2007 [PDF]
- Thema
- Übersicht: Kriterien/Dimensionen von Klassifikation, Monotonicity of Relesse etc./ What,Who,Where,When
- Abstract
- Computing systems often deliberately release (or declassify) sensitive information. A principal security concern for systems permitting information release is whether this release is safe: is it possible that the attacker compromises the information release mechanism and extracts more secret information than intended? While the security community has recognised the importance of the problem, the state-of-theart in information release is, unfortunately, a number of approaches with somewhat unconnected semantic goals. We provide a road map of the main directions of current research, by classifying the basic goals according to what information is released, who releases information, where in the system information is released, and when information can be released. With a general declassification framework as a long-term goal, we identify some prudent principles of declassification. These principles shed light on existingdefinitions and may also serve as useful "sanity checks" for emerging models.
Quantitatives IFC
- Stephen McCamant, Michael D. Ernst: Quantitative information flow as network flow capacity, PLDI 2008 [PDF]
- Thema
- Können z.B. bei realistischen Bildbearbeitungsprogrammen (ImageMagick) erkennen, ob eine bestimmte Manipulation wieder zurückgerechnet werden kann. Stichwort: Kinderschänderfoto mit Wirbel.
- Abstract
- We present a new technique for determining how much information about a program's secret inputs is revealed by its public outputs. In contrast to previous techniques based on reachability from secret inputs (tainting), it achieves a more precise quantitative result by computing a maximum flow of information between the inputs and outputs. The technique uses static control-flow regions to soundly account for implicit flows via branches and pointer operations, but operates dynamically by observing one or more program executions and giving numeric flow bounds specific to them (e.g., "17 bits"). The maximum flow in a network also gives a minimum cut (a set of edges that separate the secret input from the output), which can be used to efficiently check that the same policy is satisfied on future executions. We performed case studies on 5 real C, C++, and Objective C programs, 3 of which had more than 250K lines of code. The tool checked multiple security policies, including one that was violated by a previously unknown bug.
- David Clark, Sebastian Hunt, Pasquale Malacaria: Quantified Interference for a While Language, Electronic Notes in Theoretical Computer Science 2005 [PDF]
- Thema
- Basis für quantitatives IFC fuer eine while-Sprache. Anderer Ansatz wie McCamant, Ernst.
- Abstract
- We show how information theory can be used to give a quantitative definition of interference between variables in imperative programming languages. In this paper we focus on a particular case of this definition of interference: leakage of information from private variables to public ones in While language programs. The major result of the paper is a quantitative analysis for this language that employs a use-definition graph to calculate bounds on the leakage into each variable.
Taint-Analyse
- Marco Pistoia, Robert J. Flynn, Larry Koved, Vugranam C. Sreedhar: Interprocedural Analysis for Privileged Code Placement and Tainted Variable Detection, ECOOP 2005 [PDF]
- Thema
- Taint Analyse mit Slicing
- Abstract
- In Java 2 and Microsoft .NET Common Language Runtime (CLR), trusted code has often been programmed to perform access-restricted operations not explicitly requested by its untrusted clients. Since an untrusted client will be on the call stack when access control is enforced, an access-restricted operation will not succeed unless the client is authorized. To avoid this, a portion of the trusted code can be made “privileged.” When access control is enforced, privileged code causes the stack traversal to stop at the trusted code frame, and the untrusted code stack frames will not be checked for authorization. For large programs, manually understanding which portions of code should be made privileged is a difficult task. Developers must understand which authorizations will implicitly be extended to client code and make sure that the values of the variables used by the privileged code are not “tainted” by client code. This paper presents an interprocedural analysis for Java bytecode to automatically identify which portions of trusted code should be made privileged, ensure that there are no tainted variables in privileged code, and detect “unnecessary” and “redundant” privileged code. We implemented the algorithm and present the results of our analyses on a set of large programs. While the analysis techniques are in the context of Java code, the basic concepts are also applicable to non-Java systems with a similar authorization model.
- James Newsome, Dawn Song: Dynamic Taint Analysis for Automatic Detection, Analysis, and Signature Generation of Exploits on Commodity Software, Distributed System Security Symposium (NDSS) 2005 [PDF]
- Thema
- Taint Analyse Basis
- Abstract
- Software vulnerabilities have had a devastating effect on the Internet. Worms such as CodeRed and Slammer can compromise hundreds of thousands of hosts within hours or even minutes, and cause millions of dollars of damage [25, 42]. To successfully combat these fast auto- matic Internet attacks, we need fast automatic attack de- tection and filtering mechanisms.
- In this paper we propose dynamic taint analysis for au- tomatic detection of overwrite attacks, which include most types of exploits. This approach does not need source code or special compilation for the monitored program, and hence works on commodity software. To demonstrate this idea, we have implemented TaintCheck, a mechanism that can perform dynamic taint analysis by performing binary rewriting at run time. We show that TaintCheck reliably detects most types of exploits. We found that TaintCheck produced no false positives for any of the many different programs that we tested. Further, we describe how Taint- Check could improve automatic signature generation in several ways.
Proof-Carrying Code (PCC) und Mobius
- Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas Jensen, David Pichardie : The MOBIUS Proof Carrying Code Infrastructure, Lecture Notes in Computer Science, 2008, Volume 5382 [PDF]
- Thema
- Mobius Projekt (http://mobius.inria.fr/): Vision - PCC für Handy-Apps
- Abstract
- The goal of the MOBIUS project is to develop a Proof Carrying Code architecture to secure global computers that consist of Java-enabled mobile devices. In this overview, we present the consumer side of the MOBIUS Proof Carrying Code infrastructure, for which we have developed formally certified, executable checkers. We consider wholesale Proof Carrying Code scenarios, in which a trusted authority verifies the certificate before cryptographically signing the application. We also discuss retail Proof Carrying Code, where the verification is performed on the consumer device.
- Gilles Barthe, Benjamin Gregoire, Mariela Pavlova : Preservation of Proof Obligations from Java to the Java Virtual Machine, IJCAR 2008 [PDF]
- Thema
- Mobius Projekt (http://mobius.inria.fr/): Beweise Java Programme bleiben gueltig, wenn sie zu Bytecode compiliert werden.
- Abstract
- While program verification environments typically target source programs, there is an increasing need to provide strong guarantees for executable programs.
- We establish that it is possible to reuse the proof that a source Java program meets its specification to show that the corresponding JVM program, obtained by non-optimizing compilation, meets the same specification. More concretely, we show that verification condition generators for Java and JVM programs generate the same set of proof obligations, when applied to a program p and its compilation p respectively.
- Preservation of proof obligations extends the applicability of Proof Carrying Code, by allowing certificate generation to rely on existing verification technology.
- George C. Necula: Proof-carrying code, POPL 1997 [PDF]
- Thema
- Grundlage von Proof-carrying code
- Abstract
- This paper describes proof-carrying code (PCC), a mechanism by which a host system can determine with certainty that it is safe to execute a program supplied (possibly in binary form) by an untrusted source. For this to be possible, the untrusted code producer must supply with the code a safety proof that attests to the code's adherence to a previously defined safety policy. The host can then easily and quickly validate the proof without using cryptography and without consulting any external agents.In order to gain preliminary experience with PCC, we have performed several case studies. We show in this paper how proof-carrying code might be used to develop safe assembly-language extensions of ML programs. In the context of this case study, we present and prove the adequacy of concrete representations for the safety policy, the safety proofs, and the proof validation. Finally, we briefly discuss how we use proof-carrying code to develop network packet filters that are faster than similar filters developed using other techniques and are formally guaranteed to be safe with respect to a given operating system safety policy.
- Gilles Barthe, David Pichardie, Tamara Rezk : A Certified Lightweight Non-interference Java Bytecode Verifier, ESOP 2007 [PDF]
- Thema
- Non-Interference mit PCC
- Abstract
- Non-interference is a semantical condition on programs that guarantees the absence of illicit information flow throughout their execution, and that can be enforced by appropriate information flow type systems. Much of previous work on type systems for non-interference has focused on calculi or high-level programming languages, and existing type systems for low-level languages typically omit objects, exceptions, and method calls, and/or do not prove formally the soundness of the type system. We define an information flow type system for a sequential JVM-like language that includes classes, objects, arrays, exceptions and method calls, and prove that it guarantees non-interference. For increased confidence, we have formalized the proof in the proof assistant Coq; an additional benefit of the formalization is that we have extracted from our proof a certified lightweight bytecode verifier for information flow. Our work provides, to our best knowledge, the first sound and implemented information flow type system for such an expressive fragment of the JVM.
IFC mit abstrakter Interpretation
- Samir Genaim, Fausto Spoto: Information Flow Analysis for Java Bytecode, VMCAI 2005 [PDF]
- Thema
- Information Flow Control durch abstrakte Interpretation
- Abstract
- We present a flow and context sensitive compositional information flow analysis for full (mono-threaded) Java bytecode. We base our analysis on the transformation of the Java bytecode into a control-flow graph of basic blocks of code which makes explicit the complex features of the Java bytecode. We represent information flows through Boolean functions and hence implement an accurate and efficient information flow analysis through binary decision diagrams. To the best of our knowledge, it is the first one for full Java bytecode.
- Patrick Cousot: Abstract Interpretation Based Formal Methods and Future Challenges, Lecture Notes in Computer Science 2001 [PDF]
- Thema
- Grundlage: Abstrakte Interpretation
- Abstract
- In order to contribute to the solution of the software reliability problem, tools have been designed to analyze statically the run-time behavior of programs. Because the correctness problem is undecidable, some form of approximation is needed. The purpose of abstract inter- pretation is to formalize this idea of approximation. We illustrate informally the application of abstraction to the semantics of programming languages as well as to static program analysis. The main point is that in order to reason or compute about a complex system, some information must be lost, that is the observation of executions must be either partial or at a high level of abstraction.
- A few challenges for static program analysis by abstract interpretation are finally briefly discussed. The electronic version of this paper includes a comparison with other formal methods: typing, model-checking and deductive methods.
Sicherheitsanalysen für JavaScript
- Ravi Chugh, Jeffrey A. Meister, Ranjit Jhala, Sorin Lerner: Staged Information Flow for JavaScript, PLDI 2009 [PDF]
- Thema
- Staged IFC für dynamischen Code, Beispiel: import fremder JS-Bibliotheken (Ad-Scripts)
- Abstract
- Modern websites are powered by JavaScript, a flexible dynamicscripting language that executes in client browsers. A common paradigm in such websites is to include third-party JavaScript code in the form of libraries or advertisements. If this code were malicious,it could read sensitive information from the page or write to the location bar, thus redirecting the user to a malicious page, from which the entire machine could be compromised. We present an information-flow based approach for inferring the effects that a piece of JavaScript has on the website in order to ensure that key security properties are not violated. To handle dynamically loaded and generated JavaScript, we propose a framework for staging information flow properties. Our framework propagates information flow through the currently known code in order to compute a minimal set of syntactic residual checks that are performed on the remaining code when it is dynamically loaded.We have implemented a prototype framework for staging information flow. We describe our techniques for handling some difficult features of JavaScript and evaluate our system’s performance on a variety of large realworld websites. Our experiments show that static information flow is feasible and efficient for JavaScript, and that our technique allows the enforcement of information-flow policies with almost no run-time overhead.
- Salvatore Guarnieri, Benjamin Livshits: GATEKEEPER: Mostly Static Enforcement of Security and Reliability Policies for JavaScript Code, USENIX 2009 [PDF]
- Thema
- Ein von Microsoft entwickeltes Policy-enforcement System fuer JavaScript.
- Abstract
- The advent of Web 2.0 has lead to the proliferation of client-side code that is typically written in JavaScript. This code is often combined — or mashed-up — with other code and content from disparate, mutually untrusting parties, leading to undesirable security and reliability consequences.
- This paper proposes GATEKEEPER, a mostly static approach for soundly enforcing security and reliability policies for JavaScript programs. GATEKEEPER is a highly extensible system with a rich, expressive policy language, allowing the hosting site administrator to formulate their policies as succinct Datalog queries.
- The primary application of GATEKEEPER this paper explores is in reasoning about JavaScript widgets such as those hosted by widget portals Live.com and Google/IG. Widgets submitted to these sites can be either malicious or just buggy and poorly written, and the hosting site has the authority to reject the submission of widgets that do not meet the site’s security policies.
- To show the practicality of our approach, we describe nine representative security and reliability policies. Statically checking these policies results in 1,341 verified warnings in 684 widgets, no false negatives, due to the soundness of our analysis, and false positives affecting only two widgets.
Zugriffskontrolle - Access Control
- Paolina Centonze, Gleb Naumovich, Stephen J. Fink, Marco Pistoia
- Role Based Access Control Consistency Validation, ISSTA 2006 [PDF]
- Thema
- RBAC, "Passen Control-Regeln zu Datenzugriff?". Erfordert Grundwissen Datenflussanalyse (eine Kill/Gen Analyse wird gemacht)
- Wirklich verwendbare Taint Analyse fuer Webapplikationen
- Abstract
- Modern enterprise systems support Role-Based Access Control (RBAC). Although RBAC allows restricting access to privileged operations, a deployer may actually intend to re strict access to privileged data. This paper presents a theoretical foundation for correlating an operation-based RBAC policy with a data-based RBAC policy. Relying on a location-consistency property, this paper shows how to infer whether an operation-based RBAC policy is equivalent to any data-based RBAC policy. We have built a static analysis tool for Java Platform, Enterprise Edition (Java EE) called Static Analysis for Validation of Enterprise Security (SAVES). Relying on interprocedural pointer analysis and dataflow analysis, SAVES analyzes Java EE bytecode to determine if the associated RBAC policy is location consistent, and reports potential security Flaws where location consistency does not hold. The experimental results obtained by using SAVES on a number of production-level Java EE codes have identified several security Flaws with no false positive reports.
- Zusätzlich: Erläuterung von Access Control und Übersicht über die verschiedenen Arten mit ihren Vor- und Nachteilen. Siehe A survey of static analysis methods for identifying security vulnerabilities in software systems [PDF] sowie einschlägige Lehrbücher.