Abstract Distributed applications are difficult to program reliably and securely. Dependently typed functional languages promise to prevent broad classes of errors and vulnerabilities, and to enable program verification to proceed side-by-side with development. However, as recursion, effects, and rich libraries are added, using types to reason about programs, specifications, and proofs becomes challenging. We present F*, a full-fledged design and implementation of a new dependently typed language for secure distributed programming. Our language provides arbitrary recursion while maintaining a logically consistent core; it enables modular reasoning about state and other effects using affine types; and it supports proofs of refinement properties using a mixture of cryptographic evidence and logical proof terms. The key mechanism is a new kind system that tracks several sub-languages within F* and controls their interaction. F* subsumes two previous languages, F7 and Fine. We prove type soundness (with proofs mechanized in Coq) and logical consistency for F*. We have implemented a compiler that translates F* to .NET bytecode, based on a prototype for Fine. F* provides access to libraries for concurrency, networking, cryptography, and interoperability with C#, F#, and the other .NET languages. The compiler produces verifiable binaries with 60% code size overhead for proofs and types, as much as a 45x improvement over the Fine compiler, while still enabling efficient bytecode verification. We have programmed and verified nearly 50,000 lines of F* including new schemes for multi-party sessions; a zero-knowledge privacy-preserving payment protocol; a provenance-aware curated database; a suite of web-browser extensions verified for authorization properties; a cloud-hosted multi-tier web application with a verified reference monitor; the core F* typechecker itself; and programs translated to F* from other languages such as F7 and JavaScript.
In nanometer technology regime, design components mandate their reuse to meet the complex design challenges and hence comprise Intellectual Property (IP). Unauthorized reuse raises major security issues. IP mark(s) is embedded into a design for establishing the veracity of a legal IP owner/buyer. However, methods for trustworthy public verification of IP marks are not secure. For field-programmable gate-array (FPGA) designs, marks become prone to tampering, and even being overridden by an attacker's signature after public verification. In order to ensure trustworthy yet leakage-proof public verification based on the marks hidden in a FPGA design, we propose a zero-knowledge protocol Verify_ZKP. It is an interactive two-person game between the prover and the verifier. This protocol is fast, incurs no additional design overhead, and needs no centralized signature database. We establish that Verify_ZKP satisfies zero-knowledge property, and introduce statistical metrics to measure its robustness. We have simulated our protocol for IWLS'05 FPGA benchmarks. Experimental results on robustness and overhead are very encouraging.
Physical Unclonable Functions (PUFs) and Hardware Security
Concepts for future energy networks envision the distribution of measurement and control infrastructures to the customers to allow for improved reactions to certain events in the energy grid and to ease the measurement process. Such a distribution of control functionalities requires a corresponding device on the customer side that performs or mediates between the energy grid requirements and the customer infrastructure. These Smart Energy Gateways (SEGs) are owned by the energy network operator and but enforce the contracts between network operator and customer for both parties. They can also support additional value-added services. Due to the different uses, SEGs will be exposed to more and other attacks than current end-user devices such as DSL or WLAN routers. The impact of attacks to SEGs is also a peril to the overall operation of the energy grid. This paper provides an approach to the reliable identification of SEGs based on already established industry standards, namely Trusted Computing and Trusted Network Connect.
Applications on multi-application smart cards contain sensitive data and can exchange information. Thus a major concern is that these applications should not exchange data unless permitted by their respective policy. As modern smart cards allow post-issuance installation and removal of applications, traditional approaches for information flow analysis are not suitable. We suggest the Security-by-Contract approach for loading time application certification on the card, that will enable the stakeholders with the means to ensure the compliance of every update of the card with their security policy. We describe an extension of the card security architecture to deal with verification for different types of updates and present a Java Card prototype implementation of the Policy Checker with performance measurements.
L'interpretazione astratta è una teoria che formalizza l'approssimazione conservativa della semantica di sistemi informatici hardware e software, focalizzandosi su alcune proprietà, che espresse mediante opportune strutture algebriche (domini astratti) possono essere calcolate in modo corretto (anche se non completo). Una grande varietà di domini astratti può essere elaborata, a aseconda dei contesti di applicazione, e con scelta dei domini astratti è possibile modulare in modi diversi precisione e complessità computazionale. Questa tesi considera l'applicazione di tecniche di Interpretazione Astratta in tre diversi scenari: Program slicing; Watermarking di database relazionali; Watermarking del codice sorgente di programmi. Relativamente al Program slicing, viene proposto un raffinamento delle tecniche tradizionali già presenti in letteratura. Molto spesso, siamo interessati a una specifica proprietà delle variabili in un criterio di slicing, piuttosto che ai suoi effettivi valori. Questo è il caso, ad esempio, quando si analizza la non-interferenza in language-based security, dove le astrazioni entrano in gioco per modellare il potere osservativo degli attaccanti. In questo scenario, lo slicing tiene in considerazione le proprietà astratte delle variabili e le dipendenze astratte. Questo approccio allo slicing, non è solo la generalizzazione della tecnica tradizionale, ma offre nuovi spunti nelle relazioni tra diverse aree di ricerca dell'informatica. Un secondo scenario di applicazione delle tecniche di Interpretazione Astratta è la progettazione di watermarking di database relazionali, la cui rilevanza è legata al fatto che in Internet è molto importante preservare i diritti di proprietà nei database relazionali mantenuti in outsourcing. In tale ambito, viene proposta una tecnica di watermarking senza distorsione, che migliora la verifica dell'integrità dei database relazionali utilizzando un meccanismo di autenticazione pubblica. L'ultimo scenario considerato è quello del Watermarking del codice sorgente di programmi: all'aumentare della quantità di codice sorgente distribuito sul web, la protezione e il rilevamento delle proprietà del software è diventata una questione importante. Nella tesi, viene presentato uno schema di watermarking software a chiave pubblica (watermarking asimmetrico), basato su tecniche di trasformazione che preservano la semantica, e che è simile nello spirito alle zero-knowledge proofs. L'approccio proposto si pone come un'alternativa alla cifratura e l'autenticazione software piuttosto che come uno strumento per la protezione del copyright.
Abstract. In resetting attacks against a proof system, a prover or a verifier is reset and enforced to use the same random tape on various inputs as many times as an adversary may want. Recent deployment of cloud computing gives these attacks a new importance. This paper shows that argument systems for any NP language that are both resettably-sound and resettable zero-knowledge are possible by a constant-round protocol in the BPK model. For that sake, we define and construct a resettablyextractable conditional commitment scheme.
We propose a coin-flip protocol which yields a string of strong, random coins and is fully simulatable against poly-sized quantum adversaries on both sides. It can be implemented with quantum-computational security without any set-up assumptions, since our construction only assumes mixed commitment schemes which we show how to construct in the given setting. We then show that the interactive generation of random coins at the beginning or during outer protocols allows for quantum-secure realizations of classical schemes, again without any set-up assumptions. As example applications we discuss quantum zero-knowledge proofs of knowledge and quantum-secure two-party function evaluation. Both applications assume only fully simulatable coin-flipping and mixed commitments. Since our framework allows to construct fully simulatable coin-flipping from mixed commitments, this in particular shows that mixed commitments are complete for quantum-secure two-party function evaluation. This seems to be the first completeness result for quantum-secure two-party function evaluation from a generic assumption.
We present a method to compile Yao’s two-player garbled circuit protocol into one that is secure against malicious adversaries that relies on witness indistinguishability. Our approach can enjoy lower communication and computation overhead than methods based on cut-andchoose [13] and lower overhead than methods based on zero-knowledge proofs [8] (or Σ-protocols [14]). To do so, we develop and analyze new solutions to issues arising with this transformation: — How to guarantee the generator’s input consistency — How to support different outputs for each player without adding extra gates to the circuit of the function f being computed — How the evaluator can retrieve input keys but avoid selective failure attacks — Challenging 3/5 of the circuits is near optimal for cut-and-choose (and better than challenging 1/2) Our protocols require the existence of secure-OT and claw-free functions that have a weak malleability property. We discuss an experimental implementation of our protocol to validate our efficiency claims.
Imad Fakhri Taha Alshaikhli, Rusydi Hasan Makarin, Siti Khairunnisa Mohd Bakri, Nur Dalilah More Yusoff · 5 authors
Much of the current innovation in advanced materials is occurring at the nanoscale, specifically in manufactured nanomaterials (MNs). MNs display unique attributes and behaviors, and may be biologically and physically unique, making them valuable across a wide range of applications. However, as the number, diversity and complexity of MNs coming to market continue to grow, assessing their health and environmental risks with traditional animal testing approaches is too time- and cost-intensive to be practical, and is undesirable for ethical reasons. New approaches are needed that meet current requirements for regulatory risk assessment while reducing reliance on animal testing and enabling safer-by-design product development strategies to be implemented. The adverse outcome pathway (AOP) framework presents a sound model for the advancement of MN decision making. Yet, there are currently gaps in technical and policy aspects of AOPs that hinder the adoption and use for MN risk assessment and regulatory decision making. This review outlines the current status and next steps for the development and use of the AOP framework in decision making regarding the safety of MNs. Opportunities and challenges are identified concerning the advancement and adoption of AOPs as part of an integrated approach to testing and assessing (IATA) MNs, as are specific actions proposed to advance the development, use and acceptance of the AOP framework and associated testing strategies for MN risk assessment and decision making. The intention of this review is to reflect the views of a diversity of stakeholders including experts, researchers, policymakers, regulators, risk assessors and industry representatives on the current status, needs and requirements to facilitate the future use of AOPs in MN risk assessment. It incorporates the views and feedback of experts that participated in two workshops hosted as part of an Organization for Economic Cooperation and Development (OECD) Working Party on Manufactured Nanomaterials (WPMN) project titled, "Advancing AOP Development for Nanomaterial Risk Assessment and Categorization", as well as input from several EU-funded nanosafety research consortia.
Abstract. This paper proposes a novel method for watermarking C source code by exploiting the programming language features.The key idea of our watermarking scheme is a semantics-preserving program transformation, based on a hidden permutation of local identifiers, followed by another hidden permutation of the functions defined in the source code. This last permutation allows to encrypt the prove of ownership, in the framework of interactive zero-knowledge proof system. The proposed watermarking scheme is invisible to compilers and does not reveal any information about the watermark, its nature and its location into the program, since the zero knowledge proof is independent of the encoding and of the embedding. Finally, we introduce a third party Trusted Time-Stamp Service into the system to prevent invertibility/ambiguity attacks.
Advanced Malware Detection Techniques
Security and Verification in Computing
Physical Unclonable Functions (PUFs) and Hardware Security
This paper presents a property attestation protocol for the security chip TCM (trusted cryptographic module) via analyzing the problems of the current property attestation, which is built on the property attestation model with the online trust third party. In the protocol the prover utilizes the zero-knowledge proof by the attribute certificates, configuration commitment and TCM signature, and attests its configuration and status which are compliant with the declarative security property. The protocol is characterized by shorter signature length and lower computations. The security of the protocol is proved at the random oracle model. The protocol can help extend application and improve standard for security chip TCM, and it also has practical value and immediate significance.
Abstract. The concept of zero-knowledge proofs has been around for about 25 years. It has been redefined over and over to suit the special security requirements of protocols and systems. Common among all definitions is the requirement of the existence of some efficient “device ” simulating the view of the verifier (or the transcript of the protocol), such that the simulation is indistinguishable from the reality. The definitions differ in many respects, including the type and power of the devices, the order of quantifiers, the type of indistinguishability, and so on. In this paper, we will scrutinize the definition of “black-box computational ” zero-knowledge, in which there exists one simulator for all verifiers, the simulator has black-box access to the verifier, and the quality of simulation is such that the real and simulated views cannot be distinguished by polynomial tests (computational indistinguisha-bility). Working in a theoretical model (the Random-Oracle Model), we show that the indistinguishability requirement is stated in a conceptually inappropriate way: Present definitions allow the knowledge of the verifier and distin-guisher to be independent, while the two entities are essentially coupled. Therefore, our main take on the problem will be conceptual and semantic, rather than literal. We formalize the concept by introducing a “knowledge ex-tractor ” into the model, which tries to extract the extra knowledge hard-coded into the distinguisher (if any), and then helps the simulator to construct the view of the verifier. The new paradigm is termed Simulation-Extraction
In order to solve the issue that existing direct anonymous attestation (DAA) scheme can not operate effectively in different domains,based on the original DAA scheme,a novel direct anonymous attestation protocol used in multi domains environment is proposed and designed,in which,the certificate issuer located in outside of domain can be considered as a proxy server to issue the DAA certificate for valid member nodes directly.Our designed mechanism accords with present trusted computing group (TCG) international specification,and can solve the problems of practical authentication and privacy information protection between different trusted domains efficiently.Compared with present DAA scheme,in our protocol,the anonymity,unforgeability can be guaranteed,and the replay-attack also can be avoided.It has important referenced and practical application value in trusted computing field.
Endre Bangerter, Stephan Krenn, Ahmad‐Reza Sadeghi, Thomas Schneider · 5 authors
Abstract. Zero-knowledge proofs of knowledge (ZK-PoK) play an important role in many cryptographic applications. Direct anonymous attestation (DAA) and the identity mixer anonymous authentication system are first real world applications using ZK-PoK as building blocks. But although being used for many years now, design and implementation of sound ZK-PoK remains challenging. In fact, there are security flaws in various protocols found in literatur. Especially for non-experts in the field it is often hard to design ZK-PoK, since a unified and easy to use theoretical framework on ZK-PoK is missing. With this paper we overcome important challenges and facilitate the design and implementation of efficient and sound ZK-PoK in practice. First, Camenisch et al. have presented at EUROCRYPT 2009 a first unified and modular theoretical framework for ZK-PoK. This is compelling, but makes use of a rather inefficient 6-move protocol. We extend and improve their framework in terms of efficiency and show how to realize it using efficient 3-move Σ-protocols. Second, we perform an exact security and efficiency analysis for our new protocol and various protocols found in the literature. The analysis yields novel- and perhaps surprising- results and insights. It reveals for instance that using a 2048 bit RSA modulus, as specified in the DAA standard, only guarantees an upper bound on the success probability of a malicious prover between 1/2 4 and 1/2 24. Also, based on that analysis we show how to select the most efficient protocol to realize a given proof goal. Finally, we also provide low-level support to a designer by presenting a compiler realizing our framework and optimization techniques, allowing easy implementation of efficient and sound protocols.
Abstract : University of North Texas (UNT) is collaborating with the Air Force Research Laboratory (AFRL) in the design and development of ZKP protocol and in investigating its suitability for airborne networks. During this project, we accomplished the following tasks: (1) Implemented a prototype version of graph isomorphism based ZKP protocol. (2) Analyzed the implementation complexity of the ZKP protocol. (3) Investigated the selection of graphs that are suitable for ZKP implementation. Our experiments related to task (3) indicate that the graphs selected for ZKP implementation must possess specific characteristics. While we developed the basic guidelines for this selection, our results are inconclusive and require additional experiments.