Clever algorithm design is sometimes superseded by simple encodings into logic. We apply this motto to a few case studies in the formal verification of security properties. In particular, we examine confidentiality objectives in hardware circuit descriptions written in VHDL.
This paper provides a Hoare-style logic for quantum computation. While the usual Hoare logic helps us to verify classical deterministic programs, our logic supports quantum probabilistic programs. Our target programming language is QPL defined by Selinger, and our logic is an extension of the probabilistic Hoare-style logic defined by den Hartog. In this paper, we demonstrate how the quantum Hoare-style logic proves properties of well-known algorithms.
Proxy signature is an important delegation technology. In this paper, we proposed a novel proxy signature scheme with multi-warrant by extending proxy signature. This extension is not a trivial extension, it makes that the size of extended proxy signature is approximate one of original proxy signature. And the size of the extended proxy signature is constant and is independent of warrant’s number. The scheme is proven secure in the standard model and the security of the scheme is related to the Computational Diffie-Hellman Assumption. Comparison with Huang et.al scheme, our scheme has an advantage over Huang et.al’s scheme in terms of the size of proxy signature.
Language-based information flow analysis is used to statically examine a program for information flows between objects of different security domains, and to verify these flows follow a given policy. When the program is distributed as mobile code, it may access resources whose domains depend on the client environment, or may face different security policies. In proof-carrying code scenarios, it is desirable to give a single proof that the program executes securely in any of these situations. This paper presents an object-oriented, Java-like language with runtime security types that can be inspected to ensure that flows between accessed objects are actually allowed before operations inducing these flows are performed. A type system is used to statically prove that the flow tests included in the program are sufficient, such that a noninterference property for the program is ensured regardless of the domains of objects and the effective security policy. Also, the paper outlines how the concepts of the type system are transferred to a bytecode language.
Designing symmetric ciphers based on chaotic maps or cellular automata has a long but rarely successful history. In this paper, we examine some symmetric ciphers based on chaotic maps and cellular automata, and indicate how to reconcile design techniques for these primitives with current methodologies.
Static equivalence is a well established notion of indistinguishability of sequences of terms which is useful in the symbolic analysis of cryptographic protocols. Static equivalence modulo equational theories allows a more accurate representation of cryptographic primitives by modelling properties of operators by equational axioms. We develop a method that allows in some cases to simplify the task of deciding static equivalence in a multi-sorted setting, by removing a symbol from the term signature and reducing the problem to several simpler equational theories. We illustrate our technique at hand of bilinear pairings.
We presents a compositional Hoare logic for proving semantic security of modes of operation for symmetric key block ciphers. We propose a simple programming language to specify encryption modes and an assertion language that allows to state invariants and axioms and rules to establish such invariants. The assertion language consists of few atomic predicates. We were able to use our method to verify semantic security of several encryption modes including Cipher Block Chaining (CBC), Cipher Feedback mode (CFB), Output Feedback (OFB), and Counter mode (CTR).
Simulation-based security notions for cryptographic protocols are regarded as highly desirable, primarily because they admit strong composability and, consequently, a modular design. In this paper, we give a simulation-based security definition for two-round authenticated message exchange and show that a concrete protocol, 2AMEX-1, satisfies our security property, that is, we provide an ideal functionality for two-round authenticated message exchange and show that 2AMEX-1 realizes it securely. To model the involved public-key infrastructure adequately, we use a joint-state approach.
Grids are constructed to integrate different kinds of resources and services in distributed computing environments. Grid users may transfer their applications and data to remote grid nodes which are easy to be compromised. In this paper, we utilize trusted computing and virtualization technologies to construct trusted execution environments in grid systems. Grid nodes are equipped with Trusted Platform Module (TPM) and secure Virtual Machine Monitor (VMM) in order to provide a Trusted Computing Base (TCB) for job execution environment. A secure Virtual Machine (VM) for protecting job execution can be deployed into a grid node remotely. During the VM deployment, current configuration information in a grid node is reported to a remote party for remote attestation. Furthermore, encryption technologies are used to protect grid jobs during their whole lifecycle. Experiments and analysis show our method is efficient and secure.
Language-based security has been a hot research area of computer security in the last decade. It addresses various concerns about software security by using programming language techniques such as type systems and program analysis/transformation. Thus, advance in programming language research can also benefit language-based security. This paper reports some recent advance in verification techniques for higher-order programs, and discusses its applications to language-based security. More specifically, we summarize the recent result on model-checking of higher-order recursion schemes, and show how it may be applied to language-based security such as secure information flow and stack-based access control.
We propose an extension of the standard Dolev-Yao model of cryptographic protocols to facilitate symbolic reasoning about zero-knowledge proofs. This is accomplished by communicating typed terms, and providing a proof amounts to certifying that a term is of a particular type. We present a proof system for term derivability, which is employed to yield a decision procedure for checking whether a given protocol meets its zero knowledge specification.
In their work on tractable deduction systems, D. McAllester and later D. Basin and H. Ganzinger have identified a property of inference systems (the locality property) that ensures the tractability of the Entscheidungsproblem. On the other hand, deducibility constraints are sequences of deduction problems in which some parts (formulas) are unknown. The problem is to decide their satisfiability and to represent the set of all possible solutions. Such constraints have also been used for deciding some security properties of cryptographic protocols. In this paper we show that local inference systems (actually a slight modification of such systems) yield not only a tractable deduction problem, but also decidable deducibility constraints. Our algorithm not only allows to decide the existence of a solution, but also gives a representation of all solutions.
Implementing global passive adversary attacks on currently deployed low latency anonymous networks is not feasible. This paper describes the implementation of a large scale, discrete event based simulation of Tor, using the SSFNet simulator. Several global passive adversary attacks are implemented on a simulated Tor network comprised of approximately 6000 nodes. The attacks prove to be highly accurate (80 percent stream correlation rate) for low traffic conditions but significantly less effective on denser, multiplexed links (18 percent success rate).
Noninterference, which is an information flow property, is typically used as a baseline security policy to formalize confidentiality of secret information manipulated by a program. Noninterference verification mechanisms are usually based on static analyses and, to a lesser extent, on dynamic analyses. In contrast to those works, this paper proposes an information flow testing mechanism. This mechanism is sound from the point of view of noninterference. It is based on standard testing techniques and on a combination of dynamic and static analyses. Concretely, a semantics integrating a dynamic information flow analysis is proposed. This analysis makes use of static analyses results. This special semantics is built such that, once a path coverage property has been achieved on a program, a sound conclusion regarding the noninterfering behavior of the program can be established.
We investigate the problem of verifying location claims of mobile devices, and propose a new property called simultaneous distance modification (SDM). In localization protocols satisfying the SDM property, a malicious device can lie about its distance from the verifiers, but all distances can only be altered by the same amount. We demonstrate that the SDM property guarantees secure verification of location claims with a small number of verifiers even if some of them maliciously collude with the device. We also present several lightweight localization protocols that satisfy the SDM property.
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 recognized the importance of the problem, the state-of-the-art 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. We apply this classification in order to evaluate the security of a case study realized in a security-typed language: an implementation of a non-trivial cryptographic protocol that allows playing online poker without a trusted third party. In addition, we identify some prudent principles of declassification. These principles shed light on existing definitions and may also serve as useful "sanity checks" for emerging models.
For several years, various projects have collected traces of malicious activities thanks to honeypots, darknets and other Internet Telescopes. In this paper, we use the accumulated four years of data of one such system, the Leurré.com project, to assess quantitatively the influence, in these traces, of a very popular attack tool, the Metasploit Framework. We identify activities clearly related to the aforementioned exploitation tool and show the fraction of attacks this tool accounts for with respect to all other ones. Despite our initial thinking, the findings do not seem to support the assumption that such tool is only used by, so called, script kiddies. As described below, this analysis highlights the fact that a limited, yet determined, number of people are trying new exploits almost immediately when they are released. More importantly, such activity does not last for more than one or two days, as if it was all the time required to take advantage of these new exploits in a systematic way. It is worth noting that this observation is made on a worldwide scale and that the origins of the attacks are also very diverse. Intuitively, one would expect to see a kind of a Gaussian curve in the representation of the usage of these attacks by script kiddies over time, with a peak after one or two days when word of mouth has spread the rumor about the existence of a new exploit. The striking difference between this idea and the curves we obtain is an element to take into account when thinking about responsible publication of information about new exploits over the Internet.
We present a logic-based framework to evaluate the resilience of computer networks in the face of incidents, i.e., attacks from malicious intruders as well as random faults. Our model uses a two-layered presentation of dependencies between files and services, and of timed games to represent not just incidents, but also the dynamic responses from administrators and their respective delays. We demonstrate that a variant TATL◊ of timed alternating-time temporal logic is a convenient language to express several desirable properties of networks, including several forms of survivability. We illustrate this on a simple redundant Web service architecture, and show that checking such timed games against the so-called TATL◊ variant of the timed alternating time temporal logic TATL is EXPTIME-complete.
