Visible to the public Biblio

Found 5879 results

Filters: Keyword is composability  [Clear All Filters]
2022-08-26
da Costa, Patricia, Pereira, Pedro T. L., Paim, Guilherme, da Costa, Eduardo, Bampi, Sergio.  2021.  Boosting the Efficiency of the Harmonics Elimination VLSI Architecture by Arithmetic Approximations. 2021 28th IEEE International Conference on Electronics, Circuits, and Systems (ICECS). :1—4.
Approximate computing emerged as a key alternative for trading off accuracy against energy efficiency and area reduction. Error-tolerant applications, such as multimedia processing, machine learning, and signal processing, can process the information with lower-than-standard accuracy at the circuit level while still fulfilling a good and acceptable service quality at the application level. Adaptive filtering-based systems have been demonstrating high resiliency against hardware errors due to their intrinsic self-healing characteristic. This paper investigates the design space exploration of arithmetic approximations in a Very Large-Scale Integration (VLSI) harmonic elimination (HE) hardware architecture based on Least Mean Square (LMS) adaptive filters. We evaluate the Pareto front of the area- and power versus quality curves by relaxing the arithmetic precision and by adopting both approximate multipliers (AxMs) in combination with approximate adders (AxAs). This paper explores the benefits and impacts of the Dynamic Range Unbiased (DRUM), Rounding-based Approximate (RoBA), and Leading one Bit-based Approximate (LoBA) multipliers in the power dissipation, circuit area, and quality of the VLSI HE architectures. Our results highlight the LoBA 0 as the most efficient AxM applied in the HE architecture. We combine the LoBA 0 with Copy and LOA AxAs with variations in the approximation level (L). Notably, LoBA 0 and LOA with \$L=6\$ resulted in savings of 43.7% in circuit area and 45.2% in power dissipation, compared to the exact HE, which uses multiplier and adder automatically selected by the logic synthesis tool. Finally, we demonstrate that the best hardware architecture found in our investigation successfully eliminates the contaminating spurious noise (i.e., 60 Hz and its harmonics) from the signal.
Abadeh, Maryam Nooraei, Mirzaie, Mansooreh.  2021.  Ranking Resilience Events in IoT Industrial Networks. 2021 5th International Conference on Internet of Things and Applications (IoT). :1—5.
Maintaining critical data and process availability is an important challenge of Industry 4.0. Given the variety of smart nodes, data and the access latency that can be tolerated by consumers in modern IoT-based industry, we propose a method for analyzing the resiliency of an IoT network. Due to the complexity of modern system structures, different components in the system can affect the system’s resiliency. Therefore, a fundamental problem is to propose methods to quantify the value of resilience contribution of a node in each system effectively. This paper aims to identify the most critical vertices of the network with respect to the latency constraint resiliency metric. Using important centrality metrics, we identify critical nodes in industrial IoT networks to analyze the degree of resiliency in the IoT environments. The results show that when nodes with the highest value of Closeness Centrality (CC) were disrupted Resiliency of Latency (RL) would have the lowest value. In other words, the results indicate the nodes with the high values for CC are most critical in an IoT network.
Nguyen, Lan K., Nguyen, Duy H. N., Tran, Nghi H., Bosler, Clayton, Brunnenmeyer, David.  2021.  SATCOM Jamming Resiliency under Non-Uniform Probability of Attacks. MILCOM 2021 - 2021 IEEE Military Communications Conference (MILCOM). :85—90.
This paper presents a new framework for SATCOM jamming resiliency in the presence of a smart adversary jammer that can prioritize specific channels to attack with a non-uniform probability of distribution. We first develop a model and a defense action strategy based on a Markov decision process (MDP). We propose a greedy algorithm for the MDP-based defense algorithm's policy to optimize the expected user's immediate and future discounted rewards. Next, we remove the assumption that the user has specific information about the attacker's pattern and model. We develop a Q-learning algorithm-a reinforcement learning (RL) approach-to optimize the user's policy. We show that the Q-learning method provides an attractive defense strategy solution without explicit knowledge of the jammer's strategy. Computer simulation results show that the MDP-based defense strategies are very efficient; they offer a significant data rate advantage over the simple random hopping approach. Also, the proposed Q-learning performance can achieve close to the MDP approach without explicit knowledge of the jammer's strategy or attacking model.
2022-08-12
Oshnoei, Soroush, Aghamohammadi, Mohammadreza.  2021.  Detection and Mitigation of Coordinate False DataInjection Attacks in Frequency Control of Power Grids. 2021 11th Smart Grid Conference (SGC). :1—5.
In modern power grids (PGs), load frequency control (LFC) is effectively employed to preserve the frequency within the allowable ranges. However, LFC dependence on information and communication technologies (ICTs) makes PGs vulnerable to cyber attacks. Manipulation of measured data and control commands known as false data injection attacks (FDIAs) can negatively affect grid frequency performance and destabilize PG. This paper investigates the frequency performance of an isolated PG under coordinated FDIAs. A control scheme based on the combination of a Kalman filter, a chi-square detector, and a linear quadratic Gaussian controller is proposed to detect and mitigate the coordinated FDIAs. The efficiency of the proposed control scheme is evaluated under two types of scaling and exogenous FDIAs. The simulation results demonstrate that the proposed control scheme has significant capabilities to detect and mitigate the designed FDIAs.
Siu, Jun Yen, Kumar, Nishant, Panda, Sanjib Kumar.  2021.  Attack Detection and Mitigation using Multi-Agent System in the Deregulated Market. 2021 IEEE 12th Energy Conversion Congress & Exposition - Asia (ECCE-Asia). :821—826.
Over the past decade, cyber-attack events on the electricity grid are on the rise and have proven to result in severe consequences in grid operation. These attacks are becoming more intelligent and can bypass existing protection protocols, resulting in economic losses due to system operating in a falsified and non-optimal condition over a prolonged period. Hence, it is crucial to develop defense tools to detect and mitigate the attack to minimize the cost of malicious operation. This paper aims to develop a novel command verification strategy to detect and mitigate False Data Injection Attacks (FDIAs) targeting the system centralized Economic Dispatch (ED) control signals. Firstly, we describe the ED problem in Singapore's deregulated market. We then perform a risk assessment and formulate two FDIA vectors - Man in the Middle (MITM) and Stealth attack on the ED control process. Subsequently, we propose a novel verification technique based on Multi-Agent System (MAS) to validate the control commands. This algorithm has been tested on the IEEE 6-Bus 3-generator test system, and experimental results verified that the proposed algorithm can detect and mitigate the FDIA vectors.
Khan, Rafiullah, McLaughlin, Kieran, Kang, BooJoong, Laverty, David, Sezer, Sakir.  2021.  A Novel Edge Security Gateway for End-to-End Protection in Industrial Internet of Things. 2021 IEEE Power & Energy Society General Meeting (PESGM). :1—5.
Many critical industrial control systems integrate a mixture of state-of-the-art and legacy equipment. Legacy installations lack advanced, and often even basic security features, risking entire system security. Existing research primarily focuses on the development of secure protocols for emerging devices or protocol translation proxies for legacy equipment. However, a robust security framework not only needs encryption but also mechanisms to prevent reconnaissance and unauthorized access to industrial devices. This paper proposes a novel Edge Security Gateway (ESG) that provides both, communication and endpoint security. The ESG is based on double ratchet algorithm and encrypts every message with a different key. It manages the ongoing renewal of short-lived session keys and provides localized firewall protection to individual devices. The ESG is easily customizable for a wide range of industrial application. As a use case, this paper presents the design and validation for synchrophasor technology in smart grid. The ESG effectiveness is practically validated in detecting reconnaissance, manipulation, replay, and command injection attacks due to its perfect forward and backward secrecy properties.
Knesek, Kolten, Wlazlo, Patrick, Huang, Hao, Sahu, Abhijeet, Goulart, Ana, Davis, Kate.  2021.  Detecting Attacks on Synchrophasor Protocol Using Machine Learning Algorithms. 2021 IEEE International Conference on Communications, Control, and Computing Technologies for Smart Grids (SmartGridComm). :102—107.
Phasor measurement units (PMUs) are used in power grids across North America to measure the amplitude, phase, and frequency of an alternating voltage or current. PMU's use the IEEE C37.118 protocol to send telemetry to phasor data collectors (PDC) and human machine interface (HMI) workstations in a control center. However, the C37.118 protocol utilizes the internet protocol stack without any authentication mechanism. This means that the protocol is vulnerable to false data injection (FDI) and false command injection (FCI). In order to study different scenarios in which C37.118 protocol's integrity and confidentiality can be compromised, we created a testbed that emulates a C37.118 communication network. In this testbed we conduct FCI and FDI attacks on real-time C37.118 data packets using a packet manipulation tool called Scapy. Using this platform, we generated C37.118 FCI and FDI datasets which are processed by multi-label machine learning classifier algorithms, such as Decision Tree (DT), k-Nearest Neighbor (kNN), and Naive Bayes (NB), to find out how effective machine learning can be at detecting such attacks. Our results show that the DT classifier had the best precision and recall rate.
Hakim, Mohammad Sadegh Seyyed, Karegar, Hossein Kazemi.  2021.  Detection of False Data Injection Attacks Using Cross Wavelet Transform and Machine Learning. 2021 11th Smart Grid Conference (SGC). :1—5.
Power grids are the most extensive man-made systems that are difficult to control and monitor. With the development of conventional power grids and moving toward smart grids, power systems have undergone vast changes since they use the Internet to transmit information and control commands to different parts of the power system. Due to the use of the Internet as a basic infrastructure for smart grids, attackers can sabotage the communication networks and alter the measurements. Due to the complexity of the smart grids, it is difficult for the network operator to detect such cyber-attacks. The attackers can implement the attack in a manner that conventional Bad Data detection (BDD) systems cannot detect since it may not violate the physical laws of the power system. This paper uses the cross wavelet transform (XWT) to detect stealth false data injections attacks (FDIAs) against state estimation (SE) systems. XWT can capture the coherency between measurements of adjacent buses and represent it in time and frequency space. Then, we train a machine learning classification algorithm to distinguish attacked measurements from normal measurements by applying a feature extraction technique.
Sen, Ömer, Van Der Veldc, Dennis, Linnartz, Philipp, Hacker, Immanuel, Henze, Martin, Andres, Michael, Ulbig, Andreas.  2021.  Investigating Man-in-the-Middle-based False Data Injection in a Smart Grid Laboratory Environment. 2021 IEEE PES Innovative Smart Grid Technologies Europe (ISGT Europe). :01—06.
With the increasing use of information and communication technology in electrical power grids, the security of energy supply is increasingly threatened by cyber-attacks. Traditional cyber-security measures, such as firewalls or intrusion detection/prevention systems, can be used as mitigation and prevention measures, but their effective use requires a deep understanding of the potential threat landscape and complex attack processes in energy information systems. Given the complexity and lack of detailed knowledge of coordinated, timed attacks in smart grid applications, we need information and insight into realistic attack scenarios in an appropriate and practical setting. In this paper, we present a man-in-the-middle-based attack scenario that intercepts process communication between control systems and field devices, employs false data injection techniques, and performs data corruption such as sending false commands to field devices. We demonstrate the applicability of the presented attack scenario in a physical smart grid laboratory environment and analyze the generated data under normal and attack conditions to extract domain-specific knowledge for detection mechanisms.
Rai, Aditya, Miraz, MD. Mazharul Islam, Das, Deshbandhu, Kaur, Harpreet, Swati.  2021.  SQL Injection: Classification and Prevention. 2021 2nd International Conference on Intelligent Engineering and Management (ICIEM). :367—372.
With the world moving towards digitalization, more applications and servers are online hosted on the internet, more number of vulnerabilities came out which directly affects an individual and an organization financially and in terms of reputation too. Out of those many vulnerabilities such as Injection, Deserialization, Cross site scripting and more. Injection stand top as the most critical vulnerability found in the web application. Injection itself is a broad vulnerability as it further consists of SQL Injection, Command injection, LDAP Injection, No-SQL Injection etc. In this paper we have reviewed SQL Injection, different types of SQL injection attacks, their causes and remediation to comprehend this attack.
Liu, Songsong, Feng, Pengbin, Sun, Kun.  2021.  HoneyBog: A Hybrid Webshell Honeypot Framework against Command Injection. 2021 IEEE Conference on Communications and Network Security (CNS). :218—226.
Web server is an appealing target for attackers since it may be exploited to gain access to an organization’s internal network. After compromising a web server, the attacker can construct a webshell to maintain a long-term and stealthy access for further attacks. Among all webshell-based attacks, command injection is a powerful attack that can be launched to steal sensitive data from the web server or compromising other computers in the network. To monitor and analyze webshell-based command injection, we develop a hybrid webshell honeypot framework called HoneyBog, which intercepts and redirects malicious injected commands from the front-end honeypot to the high-fidelity back-end honeypot for execution. HoneyBog can achieve two advantages by using the client-server honeypot architecture. First, since the webshell-based injected commands are transferred from the compromised web server to a remote constrained execution environment, we can prevent the attacker from launching further attacks in the protected network. Second, it facilitates the centralized management of high-fidelity honeypots for remote honeypot service providers. Moreover, we increase the system fidelity of HoneyBog by synchronizing the website files between the front-end and back-end honeypots. We implement a prototype of HoneyBog using PHP and the Apache web server. Our experiments on 260 PHP webshells show that HoneyBog can effectively intercept and redirect injected commands with a low performance overhead.
Aslanyan, Hayk, Arutunian, Mariam, Keropyan, Grigor, Kurmangaleev, Shamil, Vardanyan, Vahagn.  2020.  BinSide : Static Analysis Framework for Defects Detection in Binary Code. 2020 Ivannikov Memorial Workshop (IVMEM). :3–8.

Software developers make mistakes that can lead to failures of a software product. One approach to detect defects is static analysis: examine code without execution. Currently, various source code static analysis tools are widely used to detect defects. However, source code analysis is not enough. The reason for this is the use of third-party binary libraries, the unprovability of the correctness of all compiler optimizations. This paper introduces BinSide : binary static analysis framework for defects detection. It does interprocedural, context-sensitive and flow-sensitive analysis. The framework uses platform independent intermediate representation and provide opportunity to analyze various architectures binaries. The framework includes value analysis, reaching definition, taint analysis, freed memory analysis, constant folding, and constant propagation engines. It provides API (application programming interface) and can be used to develop new analyzers. Additionally, we used the API to develop checkers for classic buffer overflow, format string, command injection, double free and use after free defects detection.

Liyanarachchi, Lakna, Hosseinzadeh, Nasser, Mahmud, Apel, Gargoom, Ameen, Farahani, Ehsan M..  2020.  Contingency Ranking Selection using Static Security Performance Indices in Future Grids. 2020 Australasian Universities Power Engineering Conference (AUPEC). :1–6.

Power system security assessment and enhancement in grids with high penetration of renewables is critical for pragmatic power system planning. Static Security Assessment (SSA) is a fast response tool to assess system stability margins following considerable contingencies assuming post fault system reaches a steady state. This paper presents a contingency ranking methodology using static security indices to rank credible contingencies considering severity. A Modified IEEE 9 bus system integrating renewables was used to test the approach. The static security indices used independently provides accurate results in identifying severe contingencies but further assessment is needed to provide an accurate picture of static security assessment in an increased time frame of the steady state. The indices driven for static security assessment could accurately capture and rank contingencies with renewable sources but due to intermittency of the renewable source various contingency ranking lists are generated. This implies that using indices in future grids without consideration on intermittent nature of renewables will make it difficult for the grid operator to identify severe contingencies and assist the power system operator to make operational decisions. This makes it necessary to integrate the behaviour of renewables in security indices for practical application in real time security assessment.

Medeiros, Ibéria, Neves, Nuno.  2020.  Impact of Coding Styles on Behaviours of Static Analysis Tools for Web Applications. 2020 50th Annual IEEE-IFIP International Conference on Dependable Systems and Networks-Supplemental Volume (DSN-S). :55–56.

Web applications have become an essential resource to access the services of diverse subjects (e.g., financial, healthcare) available on the Internet. Despite the efforts that have been made on its security, namely on the investigation of better techniques to detect vulnerabilities on its source code, the number of vulnerabilities exploited has not decreased. Static analysis tools (SATs) are often used to test the security of applications since their outcomes can help developers in the correction of the bugs they found. The conducted investigation made over SATs stated they often generate errors (false positives (FP) and false negatives (FN)), whose cause is recurrently associated with very diverse coding styles, i.e., similar functionality is implemented in distinct manners, and programming practices that create ambiguity, such as the reuse and share of variables. Based on a common practice of using multiple forms in a same webpage and its processing in a single file, we defined a use case for user login and register with six coding styles scenarios for processing their data, and evaluated the behaviour of three SATs (phpSAFE, RIPS and WAP) with them to verify and understand why SATs produce FP and FN.

Li, Ziqing, Feng, Guiling.  2020.  Inter-Language Static Analysis for Android Application Security. 2020 IEEE 3rd International Conference on Information Systems and Computer Aided Education (ICISCAE). :647–650.

The Android application market will conduct various security analysis on each application to predict its potential harm before put it online. Since almost all the static analysis tools can only detect malicious behaviors in the Java layer, more and more malwares try to avoid static analysis by taking the malicious codes to the Native layer. To provide a solution for the above situation, there's a new research aspect proposed in this paper and defined as Inter-language Static Analysis. As all the involved technologies are introduced, the current research results of them will be captured in this paper, such as static analysis in Java layer, binary analysis in Native layer, Java-Native penetration technology, etc.

Zhang, Yanmiao, Ji, Xiaoyu, Cheng, Yushi, Xu, Wenyuan.  2019.  Vulnerability Detection for Smart Grid Devices via Static Analysis. 2019 Chinese Control Conference (CCC). :8915–8919.
As a modern power transmission network, smart grid connects abundant terminal devices and plays an important role in our daily life. However, along with its growth are the security threats. Different from the separated environment previously, an adversary nowadays can destroy the power system by attacking its terminal devices. As a result, it's critical to ensure the security and safety of terminal devices. To achieve it, detecting the pre-existing vulnerabilities in the terminal program and enhancing its security, are of great importance and necessity. In this paper, we introduce Cker, a novel vulnerability detection tool for smart grid devices, which generates an program model based on device sources and sets rules to perform model checking. We utilize the static analysis to extract necessary information and build corresponding program models. By further checking the model with pre-defined vulnerability patterns, we achieve security detection and error reporting. The evaluation results demonstrate that our method can effectively detect vulnerabilities in smart devices with an acceptable accuracy and false positive rate. In addition, as Cker is realized by pure python, it can be easily scaled to other platforms.
Fan, Chengwei, Chen, Zhen, Wang, Xiaoru, Teng, Yufei, Chen, Gang, Zhang, Hua, Han, Xiaoyan.  2019.  Static Security Assessment of Power System Considering Governor Nonlinearity. 2019 IEEE Innovative Smart Grid Technologies - Asia (ISGT Asia). :128–133.
Static security assessment is of great significance to ensure the stable transmission of electric power and steady operation of load. The scale of power system trends to expand due to the development of interconnected grid, and the security analysis of the entire network has become time-consuming. On the basis of synthesizing the efficiency and accuracy, a new method is developed. This method adopts a novel dynamic power flow (DPF) model considering the influence of governor deadband and amplitude-limit on the steady state quantitatively. In order to reduce the computation cost, a contingency screening algorithm based on binary search method is proposed. Static security assessment based on the proposed DPF models is applied to calculate the security margin constrained by severe contingencies. The ones with lower margin are chosen for further time-domain (TD) simulation analysis. The case study of a practical grid verifies the accuracy of the proposed model compared with the conventional one considering no governor nonlinearity. Moreover, the test of a practical grid in China, along with the TD simulation, demonstrates that the proposed method avoids massive simulations of all contingencies as well as provides detail information of severe ones, which is effective for security analysis of practical power grids.
Liu, Kui, Koyuncu, Anil, Kim, Dongsun, Bissyandè, Tegawende F..  2019.  AVATAR: Fixing Semantic Bugs with Fix Patterns of Static Analysis Violations. 2019 IEEE 26th International Conference on Software Analysis, Evolution and Reengineering (SANER). :1–12.
Fix pattern-based patch generation is a promising direction in Automated Program Repair (APR). Notably, it has been demonstrated to produce more acceptable and correct patches than the patches obtained with mutation operators through genetic programming. The performance of pattern-based APR systems, however, depends on the fix ingredients mined from fix changes in development histories. Unfortunately, collecting a reliable set of bug fixes in repositories can be challenging. In this paper, we propose to investigate the possibility in an APR scenario of leveraging code changes that address violations by static bug detection tools. To that end, we build the AVATAR APR system, which exploits fix patterns of static analysis violations as ingredients for patch generation. Evaluated on the Defects4J benchmark, we show that, assuming a perfect localization of faults, AVATAR can generate correct patches to fix 34/39 bugs. We further find that AVATAR yields performance metrics that are comparable to that of the closely-related approaches in the literature. While AVATAR outperforms many of the state-of-the-art pattern-based APR systems, it is mostly complementary to current approaches. Overall, our study highlights the relevance of static bug finding tools as indirect contributors of fix ingredients for addressing code defects identified with functional test cases.
Pathak, Abhishek, Sivakumar, Kaarthik, Haque, Mazhar, Ganesan, Prasanna.  2019.  Multi-Cluster Visualization and Live Reporting of Static Analysis Security Testing (SAST) Warnings. 2019 IEEE Cybersecurity Development (SecDev). :145–145.
This short paper discusses a case study of multi cluster visualization of Static Analysis Security Testing (SAST) warnings in large clusters catering to a majority of Cisco products in hierarchical organizational and checker views. This serves as a one stop shop for real-time visualization of Static Analysis (SA) warning trends, chart, downloading reports, and to effectively address the potential security weaknesses detected. Presently leading SAST tools like Coverity, codesonar, Klocwork etc do not provide inter-cluster or enterprise-wide visualization to effectively address the SA warnings.
Sachidananda, Vinay, Bhairav, Suhas, Ghosh, Nirnay, Elovici, Yuval.  2019.  PIT: A Probe Into Internet of Things by Comprehensive Security Analysis. 2019 18th IEEE International Conference On Trust, Security And Privacy In Computing And Communications/13th IEEE International Conference On Big Data Science And Engineering (TrustCom/BigDataSE). :522–529.
One of the major issues which are hindering widespread and seamless adoption of Internet of Thing (IoT) is security. The IoT devices are vulnerable and susceptible to attacks which became evident from a series of recent large-scale distributed denial-of-service (DDoS) attacks, leading to substantial business and financial losses. Furthermore, in order to find vulnerabilities in IoT, there is a lack of comprehensive security analysis framework. In this paper, we present a modular, adaptable and tunable framework, called PIT, to probe IoT systems at different layers of design and implementation. PIT consists of several security analysis engines, viz., penetration testing, fuzzing, static analysis, and dynamic analysis and an exploitation engine to discover multiple IoT vulnerabilities, respectively. We also develop a novel grey-box fuzzer, called Applica, as a part of the fuzzing engine to overcome the limitations of the present day fuzzers. The proposed framework has been evaluated on a real-world IoT testbed comprising of the state-of-the-art devices. We discovered several network and system-level vulnerabilities such as Buffer Overflow, Denial-of-Service, SQL Injection, etc., and successfully exploited them to demonstrate the presence of security loopholes in the IoT devices.
Berman, Maxwell, Adams, Stephen, Sherburne, Tim, Fleming, Cody, Beling, Peter.  2019.  Active Learning to Improve Static Analysis. 2019 18th IEEE International Conference On Machine Learning And Applications (ICMLA). :1322–1327.
Static analysis tools are programs that run on source code prior to their compilation to binary executables and attempt to find flaws or defects in the code during the early stages of development. If left unresolved, these flaws could pose security risks. While numerous static analysis tools exist, there is no single tool that is optimal. Therefore, many static analysis tools are often used to analyze code. Further, some of the alerts generated by the static analysis tools are low-priority or false alarms. Machine learning algorithms have been developed to distinguish between true alerts and false alarms, however significant man hours need to be dedicated to labeling data sets for training. This study investigates the use of active learning to reduce the number of labeled alerts needed to adequately train a classifier. The numerical experiments demonstrate that a query by committee active learning algorithm can be utilized to significantly reduce the number of labeled alerts needed to achieve similar performance as a classifier trained on a data set of nearly 60,000 labeled alerts.
Aumayr, Lukas, Maffei, Matteo, Ersoy, Oğuzhan, Erwig, Andreas, Faust, Sebastian, Riahi, Siavash, Hostáková, Kristina, Moreno-Sanchez, Pedro.  2021.  Bitcoin-Compatible Virtual Channels. 2021 IEEE Symposium on Security and Privacy (SP). :901–918.
Current permissionless cryptocurrencies such as Bitcoin suffer from a limited transaction rate and slow confirmation time, which hinders further adoption. Payment channels are one of the most promising solutions to address these problems, as they allow the parties of the channel to perform arbitrarily many payments in a peer-to-peer fashion while uploading only two transactions on the blockchain. This concept has been generalized into payment channel networks where a path of payment channels is used to settle the payment between two users that might not share a direct channel between them. However, this approach requires the active involvement of each user in the path, making the system less reliable (they might be offline), more expensive (they charge fees per payment), and slower (intermediaries need to be actively involved in the payment). To mitigate this issue, recent work has introduced the concept of virtual channels (IEEE S&P’19), which involve intermediaries only in the initial creation of a bridge between payer and payee, who can later on independently perform arbitrarily many off-chain transactions. Unfortunately, existing constructions are only available for Ethereum, as they rely on its account model and Turing-complete scripting language. The realization of virtual channels in other blockchain technologies with limited scripting capabilities, like Bitcoin, was so far considered an open challenge.In this work, we present the first virtual channel protocols that are built on the UTXO-model and require a scripting language supporting only a digital signature scheme and a timelock functionality, being thus backward compatible with virtually every cryptocurrency, including Bitcoin. We formalize the security properties of virtual channels as an ideal functionality in the Universal Composability framework and prove that our protocol constitutes a secure realization thereof. We have prototyped and evaluated our protocol on the Bitcoin blockchain, demonstrating its efficiency: for n sequential payments, they require an off-chain exchange of 9+2n transactions or a total of 3524+695n bytes, with no on-chain footprint in the optimistic case. This is a substantial improvement compared to routing payments in a payment channel network, which requires 8n transactions with a total of 3026n bytes to be exchanged.
Tairi, Erkan, Moreno-Sanchez, Pedro, Maffei, Matteo.  2021.  A2L: Anonymous Atomic Locks for Scalability in Payment Channel Hubs. 2021 IEEE Symposium on Security and Privacy (SP). :1834–1851.
Payment channel hubs (PCHs) constitute a promising solution to the inherent scalability problem of blockchain technologies, allowing for off-chain payments between sender and receiver through an intermediary, called the tumbler. While state-of-the-art PCHs provide security and privacy guarantees against a malicious tumbler, they do so by relying on the scripting-based functionality available only at few cryptocurrencies, and they thus fall short of fundamental properties such as backwards compatibility and efficiency.In this work, we present the first PCH protocol to achieve all aforementioned properties. Our PCH builds upon A2L, a novel cryptographic primitive that realizes a three-party protocol for conditional transactions, where the tumbler pays the receiver only if the latter solves a cryptographic challenge with the help of the sender, which implies the sender has paid the tumbler. We prove the security and privacy guarantees of A2L (which carry over to our PCH construction) in the Universal Composability framework and present a provably secure instantiation based on adaptor signatures and randomizable puzzles. We implemented A2L and compared it to TumbleBit, the state-of-the-art Bitcoin-compatible PCH. Asymptotically, A2L has a communication complexity that is constant, as opposed to linear in the security parameter like in TumbleBit. In practice, A2L requires 33x less bandwidth than TumleBit, while retaining the computational cost (or providing 2x speedup with a preprocessing technique). This demonstrates that A2L (and thus our PCH construction) is ready to be deployed today.In theory, we demonstrate for the first time that it is possible to design a secure and privacy-preserving PCH while requiring only digital signatures and timelock functionality from the underlying scripting language. In practice, this result makes our PCH backwards compatible with virtually all cryptocurrencies available today, even those offering a highly restricted form of scripting language such as Ripple or Stellar. The practical appealing of our construction has resulted in a proof-of-concept implementation in the COMIT Network, a blockchain technology focused on cross-currency payments.
Basin, David, Lochbihler, Andreas, Maurer, Ueli, Sefidgar, S. Reza.  2021.  Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL. 2021 IEEE 34th Computer Security Foundations Symposium (CSF). :1–16.
Proofs in simulation-based frameworks have the greatest rigor when they are machine checked. But the level of details in these proofs surpasses what the formal-methods community can handle with existing tools. Existing formal results consider streamlined versions of simulation-based frameworks to cope with this complexity. Hence, a central question is how to abstract details from composability results and enable their formal verification.In this paper, we focus on the modeling of system communication in composable security statements. Existing formal models consider fixed communication patterns to reduce the complexity of their proofs. However, as we will show, this can affect the reusability of security statements. We propose an abstract approach to modeling system communication in Constructive Cryptography that avoids this problem. Our approach is suitable for mechanized verification and we use CryptHOL, a framework for developing mechanized cryptography proofs, to implement it in the Isabelle/HOL theorem prover. As a case study, we formalize the construction of a secure channel using Diffie-Hellman key exchange and a one-time-pad.
Camenisch, Jan, Dubovitskaya, Maria, Rial, Alfredo.  2021.  Concise UC Zero-Knowledge Proofs for Oblivious Updatable Databases. 2021 IEEE 34th Computer Security Foundations Symposium (CSF). :1–16.
We propose an ideal functionality FCD and a construction ΠCD for oblivious and updatable committed databases. FCD allows a prover P to read, write, and update values in a database and to prove to a verifier V in zero-knowledge (ZK) that a value is read from or written into a certain position. The following properties must hold: (1) values stored in the database remain hidden from V; (2) a value read from a certain position is equal to the value previously written into that position; (3) (obliviousness) both the value read or written and its position remain hidden from V.ΠCD is based on vector commitments. After the initialization phase, the cost of read and write operations is independent of the database size, outperforming other techniques that achieve cost sublinear in the dataset size for prover and/or verifier. Therefore, our construction is especially appealing for large datasets. In existing “commit-and-prove” two-party protocols, the task of maintaining a committed database between P and V and reading and writing values into it is not separated from the task of proving statements about the values read or written. FCD allows us to improve modularity in protocol design by separating those tasks. In comparison to simply using a commitment scheme to maintain a committed database, FCD allows P to hide efficiently the positions read or written from V. Thanks to this property, we design protocols for e.g. privacy-preserving e-commerce and location-based services where V gathers aggregate statistics about the statements that P proves in ZK.