Can we hope to provide provable security against model extraction attacks? As a step towards a theoretical study of this question, we unify and abstract a wide range of “observational” model extraction defenses (OMEDs) - roughly, those that attempt to detect model extraction by analyzing the distribution over the adversary s queries. To accompany the abstract OMED, we define the notion of complete OMEDs - when benign clients can freely interact with the model - and sound OMEDs - when adversarial clients are caught and prevented from reverse engineering the model. Our formalism facilitates a simple argument for obtaining provable security against model extraction by complete and sound OMEDs, using (average-case) hardness assumptions for PAC-learning, in a way that abstracts current techniques in the prior literature. The main result of this work establishes a partial computational incompleteness theorem for the OMED: any efficient OMED for a machine learning model computable by a polynomial size decision tree that satisfies a basic form of completeness cannot satisfy soundness, unless the subexponential Learning Parity with Noise (LPN) assumption does not hold. To prove the incompleteness theorem, we introduce a class of model extraction attacks called natural Covert Learning attacks based on a connection to the Covert Learning model of Canetti and Karchmer (TCC 21), and show that such attacks circumvent any defense within our abstract mechanism in a black-box, nonadaptive way. As a further technical contribution, we extend the Covert Learning algorithm of Canetti and Karchmer to work over any “concise” product distribution (albeit for juntas of a logarithmic number of variables rather than polynomial size decision trees), by showing that the technique of learning with a distributional inverter of Binnendyk et al. (ALT 22) remains viable in the Covert Learning setting.

Most proposals for securing control systems are heuristic in nature, and while they increase the protection of their target, the security guarantees they provide are unclear. This paper proposes a new way of modeling the security guarantees of a Cyber-Physical System (CPS) against arbitrary false command attacks. As our main case study, we use the most popular testbed for control systems security. We first propose a detailed formal model of this testbed and then show how the original configuration is vulnerable to a single-actuator attack. We then propose modifications to the control system and prove that our modified system is secure against arbitrary, single-actuator attacks.

Most proposals for securing control systems are heuristic in nature, and while they increase the protection of their target, the security guarantees they provide are unclear. This paper proposes a new way of modeling the security guarantees of a Cyber-Physical System (CPS) against arbitrary false command attacks. As our main case study, we use the most popular testbed for control systems security. We first propose a detailed formal model of this testbed and then show how the original configuration is vulnerable to a single-actuator attack. We then propose modifications to the control system and prove that our modified system is secure against arbitrary, single-actuator attacks.

Provable Security - Recent research has shown that hackers can efficiently infer sensitive user activities only by observing the network traffic of smart home devices. To protect users’ privacy, researchers have designed several traffic obfuscation methods. However, existing methods usually consume high bandwidth or provide weak privacy protection. In this paper, we conduct thorough research on smart home traffic obfuscation. We first propose a fixed-value obfuscation scheme and prove that it is perfectly secure by showing the indistinguishability of user activities. Yet, fixed-value obfuscation has high bandwidth consumption. To further reduce the bandwidth consumption, we propose combining fixed-value obfuscation with Multipath TCP transmission. The security and performance of the proposed multipath fixed-value obfuscation method are theoretically analyzed. We have implemented the proposed methods and tested them on public packet traces and simulated smart home networks. The experimental results match well with the theoretical analysis.

Provable Security - Design-hiding techniques are a central piece of academic and industrial efforts to protect electronic circuits from being reverse-engineered. However, these techniques have lacked a principled foundation to guide their design and security evaluation, leading to a long line of broken schemes. In this paper, we begin to lay this missing foundation.

Provable Security - The Industrial Internet of Things (IIoT) has brought about enormous changes in both our individual ways of life and the ways in which our culture works, transforming them into an unique electronic medium. This has enormous implications for almost every facet of life, including clever logistical, smart grids, and smart cities. In particular, the amount of gadgets that are part of the Industrial Internet of Things (IIoT) is increasing at such a fast pace that numerous gadgets and sensors are constantly communicating with one another and exchanging a substantial quantity of data. The potential of spying and hijacked assaults in messaging services has grown as a result of the creation; as a direct consequence of this, protecting data privacy and security has become two key problems at the current moment. In recent years, a protocol known as certificateless signature (LCS), which is both better secured and lighter, has been more popular for use in the development of source of energy IIoT protocols. The Schnorr signature serves as the foundation for this method s underlying mechanism. In spite of this, we found that the vast majority of the currently implemented CLS schemes are susceptible to a number of widespread security flaws. These flaws include man-in-the-middle (MITM) attacks, key generation centre (KGC) compromised attacks, and distributed denial of service (DDoS) attacks. As a potential solution to the issues that have been discussed in the preceding paragraphs, we, the authors of this work, suggest an unique pairing-free provable data approach. In order to develop a revolutionary LCS scheme that is dependable and efficient, this plan takes use of the most cutting-edge blockchain technology as well as smart contracts. After that, in order to verify the dependability of our system, we simulate both Type-I and Type-II adversary and run the results through a series of tests. The findings of a system security and a summative assessment have shown that our design is capable of providing more reliable security assurance at a lower overall cost of computation (for illustration, limited by around 40.0\% at most) and transmission time (for example, reduced by around 94.7\% at most) like other proposed scheme.

Provable Security - Unlike coverage-based fuzzing that gives equal attention to every part of a code, directed fuzzing aims to direct a fuzzer to a specific target in the code, e.g., the code with potential vulnerabilities. Despite much progress, we observe that existing directed fuzzers are still not efficient as they often symbolically or concretely execute a lot of program paths that cannot reach the target code. They thus waste a lot of computational resources. This paper presents BEACON, which can effectively direct a greybox fuzzer in the sea of paths in a provable manner. That is, assisted by a lightweight static analysis that computes abstracted preconditions for reaching the target, we can prune 82.94\% of the executing paths at runtime with negligible analysis overhead (ă5h) but with the guarantee that the pruned paths must be spurious with respect to the target. We have implemented our approach, BEACON, and compared it to five state-of-the-art (directed) fuzzers in the application scenario of vulnerability reproduction. The evaluation results demonstrate that BEACON is 11.50x faster on average than existing directed grey-box fuzzers and it can also improve the speed of the conventional coverage-guided fuzzers, AFL, AFL++, and Mopt, to reproduce specific bugs with 6.31x ,11.86x, and 10.92x speedup, respectively. More interestingly, when used to test the vulnerability patches, BEACON found 14 incomplete fixes of existing CVE-identified vulnerabilities and 8 new bugs while 10 of them are exploitable with new CVE ids assigned.

Provable Security - We address logic locking, a mechanism for securing digital Integrated Circuits (ICs) from piracy by untrustworthy foundries. We discuss previous work and the state-of-the-art, and observe that, despite more than a decade of research that has gone into the topic (resulting in both powerful attacks and subsequent defenses), there is no consensus on what it means for a particular locking mechanism to be secure. This paper attempts to remedy this situation. Specifically, it formulates a definition of security for a logic locking mechanism based on indistinguishability and relates the definition to security from actual attackers in a precise and unambiguous manner. We then describe a mechanism that satisfies the definition, thereby achieving (provable) security from all prior attacks. The mechanism assumes the existence of both a puncturable pseudorandom function family and an indistinguishability obfuscator, two cryptographic primitives that exist under well-founded assumptions. The mechanism builds upon the Stripped-Functionality Logic Locking (SFLL) framework, a state-of-the-art family of locking mechanisms whose potential for ever achieving security is currently in question. Along the way, partly as motivation, we present additional results, such as a reason founded in average-case complexity for why benchmark circuits locked with a prior scheme are susceptible to the wellknown SAT attack against such schemes, and why provably thwarting the SAT attack is insufficient as a meaningful notion of security for logic locking.

Provable Security - This paper studies provable security guarantees for cyber-physical systems (CPS) under actuator attacks. Specifically, we consider safety for CPS and propose a new attack-detection mechanism based on a zeroing control barrier function (ZCBF) condition. To reduce the conservatism in its implementation, we design an adaptive recovery mechanism based on how close the state is to violating safety. We show that the attack-detection mechanism is sound, i.e., there are no false negatives for adversarial attacks. Finally, we use a Quadratic Programming (QP) approach for online recovery (and nominal) control synthesis. We demonstrate the effectiveness of the proposed method in a case study involving a quadrotor with an attack on its motors.

Provable Security - Spectre vulnerabilities violate our fundamental assumptions about architectural abstractions, allowing attackers to steal sensitive data despite previously state-of-the-art countermeasures. To defend against Spectre, developers of verification tools and compiler-based mitigations are forced to reason about microarchitectural details such as speculative execution. In order to aid developers with these attacks in a principled way, the research community has sought formal foundations for speculative execution upon which to rebuild provable security guarantees.

Provable Security - With the rapid development of cloud storage technology, effectively verifying the cloud data’s integrity becomes a major issue in cloud storage. Recently, Nayak and Tripathy proposed their cloud auditing protocol. Although the protocol is efficient, the protocol is not secure as Yu et al’s attack shows. Even if the server does not store the users’ data, it is possible to forge the provable data possession proof and pass the integrity audit. We point out the issue in their article and describe in detail the process by which the cloud server forging the proof. We finally give an improved and more secure scheme and analysis its security also.

Provable Security - The data are stored as multiple copies on different cloud servers for improving the constancy and availability as the data are being outsourced. For proving the integrity of the data of multiple copies Provable Data Possession (PDP) protocol is used. Beforehand all of the PDP protocol will be storing copies in single cloud storage server. Public key infrastructure was depended by many PDP protocols which lacks security and leads to vulnerabilities. For storing various copies on multiple different cloud server identity based provable data possession has been used. By using the homomorphic tags data are stored in multiple cloud and its integrity will be simultaneously checked. Computation Diffie-Hellman hard problem was base for our scheme. Our scheme has been the premier for the provable data possession of multifold copies on multiple various cloud. The given system model, security model was given and this experimental research proved that our PDP scheme is applicable as well as practical.

Security in the communication systems rely mainly on a trusted Public Key Infrastructure (PKI) and Certificate Authorities (CAs). Besides the lack of automation, the complexity and the cost of assigning a signed certificate to a device, several allegations against CAs have been discovered, which has created trust issues in adopting this standard model for secure systems. The automation of the servers certificate assignment was achieved by the Automated Certificate Management Environment (ACME) method, but without confirming the trust of assigned certificate. This paper presents a complete tested and implemented solution to solve the trust of the Certificates provided to the servers by using the blockchain platform for certificate validation. The Blockchain network provides an immutable data store, holding the public keys of all domain names, while resolving the trust concerns by applying an automated Blockchain-based Domain Control Validation (B-DCV) for the server and client server verification. The evaluation was performed on the Ethereum Rinkeby testnet adopting the Proof of Authority (PoA) consensus algorithm which is an improved version of Proof of Stake (Po \$S\$) applied on Ethereum 2.0 providing superior performance compared to Ethereum 1.0.

The age of data (AoD) is identified as one of the most novel and important metrics to measure the quality of big data analytics for Internet-of-Things (IoT) applications. Meanwhile, mobile edge computing (MEC) is envisioned as an enabling technology to minimize the AoD of IoT applications by processing the data in edge servers close to IoT devices. In this paper, we study the AoD minimization problem for IoT big data processing in MEC networks. We first propose an exact solution for the problem by formulating it as an Integer Linear Program (ILP). We then propose an efficient heuristic for the offline AoD minimization problem. We also devise an approximation algorithm with a provable approximation ratio for a special case of the problem, by leveraging the parametric rounding technique. We thirdly develop an online learning algorithm with a bounded regret for the online AoD minimization problem under dynamic arrivals of IoT requests and uncertain network delay assumptions, by adopting the Multi-Armed Bandit (MAB) technique. We finally evaluate the performance of the proposed algorithms by extensive simulations and implementations in a real test-bed. Results show that the proposed algorithms outperform existing approaches by reducing the AoD around 10%.