Biblio

Found 2356 results

Filters: Keyword is privacy  [Clear All Filters]
2022-05-05
Goyal, Jitendra, Ahmed, Mushtaq, Gopalani, Dinesh.  2021.  Empirical Study of Standard Elliptic Curve Domain Parameters for IoT Devices. 2021 International Conference on Electrical, Communication, and Computer Engineering (ICECCE). :1—6.
In recent times, security and privacy concerns associated with IoT devices have caught the attention of research community. The problem of securing IoT devices is immensely aggravating due to advancement in technology. These IoT devices are resource-constraint i.e. in terms of power, memory, computation, etc., so they are less capable to secure themselves. So we need a better approach to secure IoT devices within the limited resources. Several studies state that for these lightweight IoT devices Elliptic Curve Cryptography (ECC) suits perfectly. But there are several elliptic curve domain parameter standards, which may be used for different security levels. When any ECC based product is deployed then the selection of a suitable elliptic curve standard according to usability is become very important. So we have to choose one suitable standard domain parameter for the required security level. In this paper, two different elliptic curve standard domain parameters named secp256k1 and secp192k1 proposed by an industry consortium named Standards for Efficient Cryptography Group (SECG) [1] are implemented and then analyzed their performances metrics. The performance of each domain parameter is measured in computation time.
2022-02-24
Klenze, Tobias, Sprenger, Christoph, Basin, David.  2021.  Formal Verification of Secure Forwarding Protocols. 2021 IEEE 34th Computer Security Foundations Symposium (CSF). :1–16.
Today's Internet is built on decades-old networking protocols that lack scalability, reliability, and security. In response, the networking community has developed path-aware Internet architectures that solve these issues while simultaneously empowering end hosts. In these architectures, autonomous systems construct authenticated forwarding paths based on their routing policies. Each end host then selects one of these authorized paths and includes it in the packet header, thus allowing routers to efficiently determine how to forward the packet. A central security property of these architectures is path authorization, requiring that packets can only travel along authorized paths. This property protects the routing policies of autonomous systems from malicious senders.The fundamental role of packet forwarding in the Internet and the complexity of the authentication mechanisms employed call for a formal analysis. In this vein, we develop in Isabelle/HOL a parameterized verification framework for path-aware data plane protocols. We first formulate an abstract model without an attacker for which we prove path authorization. We then refine this model by introducing an attacker and by protecting authorized paths using (generic) cryptographic validation fields. This model is parameterized by the protocol's authentication mechanism and assumes five simple verification conditions that are sufficient to prove the refinement of the abstract model. We validate our framework by instantiating it with several concrete protocols from the literature and proving that they each satisfy the verification conditions and hence path authorization. No invariants must be proven for the instantiation. Our framework thus supports low-effort security proofs for data plane protocols. The results hold for arbitrary network topologies and sets of authorized paths, a guarantee that state-of-the-art automated security protocol verifiers cannot currently provide.
2021-12-20
Sahay, Rajeev, Brinton, Christopher G., Love, David J..  2021.  Frequency-based Automated Modulation Classification in the Presence of Adversaries. ICC 2021 - IEEE International Conference on Communications. :1–6.
Automatic modulation classification (AMC) aims to improve the efficiency of crowded radio spectrums by automatically predicting the modulation constellation of wireless RF signals. Recent work has demonstrated the ability of deep learning to achieve robust AMC performance using raw in-phase and quadrature (IQ) time samples. Yet, deep learning models are highly susceptible to adversarial interference, which cause intelligent prediction models to misclassify received samples with high confidence. Furthermore, adversarial interference is often transferable, allowing an adversary to attack multiple deep learning models with a single perturbation crafted for a particular classification network. In this work, we present a novel receiver architecture consisting of deep learning models capable of withstanding transferable adversarial interference. Specifically, we show that adversarial attacks crafted to fool models trained on time-domain features are not easily transferable to models trained using frequency-domain features. In this capacity, we demonstrate classification performance improvements greater than 30% on recurrent neural networks (RNNs) and greater than 50% on convolutional neural networks (CNNs). We further demonstrate our frequency feature-based classification models to achieve accuracies greater than 99% in the absence of attacks.
2022-02-07
Gülmez, Sibel, Sogukpinar, Ibrahim.  2021.  Graph-Based Malware Detection Using Opcode Sequences. 2021 9th International Symposium on Digital Forensics and Security (ISDFS). :1–5.
The impact of malware grows for IT (information technology) systems day by day. The number, the complexity, and the cost of them increase rapidly. While researchers are developing new and better detection algorithms, attackers are also evolving malware to fail the current detection techniques. Therefore malware detection becomes one of the most challenging tasks in cyber security. To increase the performance of the detection techniques, researchers benefit from different approaches. But some of them might cost a lot both in time and hardware resources. This situation puts forward fast and cheap detection methods. In this context, static analysis provides these utilities but it is important to keep detection accuracy high while reducing resource consumption. Opcodes (operational codes) are commonly used in static analysis but sometimes feature extraction from opcodes might be difficult since an opcode sequence might have a great length. Furthermore, most of the malware developers use obfuscation and encryption techniques to avoid detection methods based on static analysis. This kind of malware is called packed malware and according to common belief, packed malware should be either unpacked or analyzed dynamically in order to detect them. In this study, a graph-based malware detection method has been proposed to overcome these problems. The proposed method relies on obtaining the opcode graph of every executable file in the dataset and using them for future extraction. In this way, the proposed method reaches up to 98% detection accuracy. In addition to the accuracy rate, the proposed method makes it possible to detect packed malware without the need for unpacking or dynamic analysis.
2022-04-19
Gürcüo\u glu, O\u guz, Erdem, Mehmet Can, Çirkino\u glu, H. Ozan, Ferhanoglu, Onur, Kurt, Güne\c s Karabulut, Panayırcı, Erdal.  2021.  Improved Physical Layer Security in Visible Light Communications by Using Focused Light Emitters. 2021 29th Signal Processing and Communications Applications Conference (SIU). :1–4.

A conventional visible light communication system consists of a transmitter, a jammer that includes a few light emitting diodes, a legal listener and an eavesdropper. In this work, a similar system is designed with a collimating lens in order to create an extra layer of practical physical security measure. The use of a collimating lens makes it available to spatially limiting data transmission to an area under the lensed transmitter. Also focused data transmission through the optical lens, increases the secrecy rate. To investigate the applicability of the proposed design we designed a sample experimental setup using USRP and implemented in a laboratory environment. In the proposed set up, the receiver is in a fixed position. However, it is possible to implement an easy, practical and cheap hardware solution with respect to a beamforming type VLC that uses directional beam forming method to establish transmission to a dynamic target. In addition, it is achievable to control the size of the area where a receiver can access data by manipulating the distance between the optical lens and transmitter.

2022-02-07
Singh, Shirish, Kaiser, Gail.  2021.  Metamorphic Detection of Repackaged Malware. 2021 IEEE/ACM 6th International Workshop on Metamorphic Testing (MET). :9–16.
Machine learning-based malware detection systems are often vulnerable to evasion attacks, in which a malware developer manipulates their malicious software such that it is misclassified as benign. Such software hides some properties of the real class or adopts some properties of a different class by applying small perturbations. A special case of evasive malware hides by repackaging a bonafide benign mobile app to contain malware in addition to the original functionality of the app, thus retaining most of the benign properties of the original app. We present a novel malware detection system based on metamorphic testing principles that can detect such benign-seeming malware apps. We apply metamorphic testing to the feature representation of the mobile app, rather than to the app itself. That is, the source input is the original feature vector for the app and the derived input is that vector with selected features removed. If the app was originally classified benign, and is indeed benign, the output for the source and derived inputs should be the same class, i.e., benign, but if they differ, then the app is exposed as (likely) malware. Malware apps originally classified as malware should retain that classification, since only features prevalent in benign apps are removed. This approach enables the machine learning model to classify repackaged malware with reasonably few false negatives and false positives. Our training pipeline is simpler than many existing ML-based malware detection methods, as the network is trained end-to-end to jointly learn appropriate features and to perform classification. We pre-trained our classifier model on 3 million apps collected from the widely-used AndroZoo dataset.1 We perform an extensive study on other publicly available datasets to show our approach's effectiveness in detecting repackaged malware with more than 94% accuracy, 0.98 precision, 0.95 recall, and 0.96 F1 score.
2022-04-19
Boche, Holger, Schaefer, Rafael F., Vincent Poor, H..  2021.  Real Number Signal Processing Can Detect Denial-of-Service Attacks. ICASSP 2021 - 2021 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP). :4765–4769.
Wireless communication systems are inherently vulnerable to adversarial attacks since malevolent jammers might jam and disrupt the legitimate transmission intentionally. Of particular interest are so- called denial-of-service (DoS) attacks in which the jammer is able to completely disrupt the communication. Accordingly, it is of crucial interest for the legitimate users to detect such DoS attacks. Turing machines provide the fundamental limits of today's digital computers and therewith of the traditional signal processing. It has been shown that these are incapable of detecting DoS attacks. This stimulates the question of how powerful the signal processing must be to enable the detection of DoS attacks. This paper investigates the general computation framework of Blum-Shub-Smale machines which allows the processing and storage of arbitrary reals. It is shown that such real number signal processing then enables the detection of DoS attacks.
Mu, Jing, Jia, Xia.  2021.  Simulation and Analysis of the Influence of Artificial Interference Signal Style on Wireless Security System Performance. 2021 IEEE 4th Advanced Information Management, Communicates, Electronic and Automation Control Conference (IMCEC). 4:2106–2109.
Aimming at the severe security threat faced by information transmission in wireless communication, the artificial interference in physical layer security technology was considered, and the influence of artificial interference signal style on system information transmission security was analyzed by simulation, which provided technical accumulation for the design of wireless security transmission system based on artificial interference.
2022-02-24
Dax, Alexander, Künnemann, Robert.  2021.  On the Soundness of Infrastructure Adversaries. 2021 IEEE 34th Computer Security Foundations Symposium (CSF). :1–16.
Campus Companies and network operators perform risk assessment to inform policy-making, guide infrastructure investments or to comply with security standards such as ISO 27001. Due to the size and complexity of these networks, risk assessment techniques such as attack graphs or trees describe the attacker with a finite set of rules. This characterization of the attacker can easily miss attack vectors or overstate them, potentially leading to incorrect risk estimation. In this work, we propose the first methodology to justify a rule-based attacker model. Conceptually, we add another layer of abstraction on top of the symbolic model of cryptography, which reasons about protocols and abstracts cryptographic primitives. This new layer reasons about Internet-scale networks and abstracts protocols.We show, in general, how the soundness and completeness of a rule-based model can be ensured by verifying trace properties, linking soundness to safety properties and completeness to liveness properties. We then demonstrate the approach for a recently proposed threat model that quantifies the confidentiality of email communication on the Internet, including DNS, DNSSEC, and SMTP. Using off-the-shelf protocol verification tools, we discover two flaws in their threat model. After fixing them, we show that it provides symbolic soundness.
2022-07-29
de Souza Donato, Robson, de Aguiar, Marlius Hudson, Cruz, Roniel Ferreira, Vitorino, Montiê Alves, de Rossiter Corrêa, Maurício Beltrão.  2021.  Two-Switch Zeta-Based Single-Phase Rectifier With Inherent Power Decoupling And No Extra Buffer Circuit. 2021 IEEE Applied Power Electronics Conference and Exposition (APEC). :1830–1836.
In some single-phase systems, power decoupling is necessary to balance the difference between constant power at load side and double-frequency ripple power at AC side. The application of active power decoupling methods aim to smooth this power oscillatory component, but, in general, these methods require the addition of many semiconductor devices and/or energy storage components, which is not lined up with achieving low cost, high efficiency and high power quality. This paper presents the analysis of a new single-phase rectifier based on zeta topology with power decoupling function and power factor correction using only two active switches and without extra reactive components. Its behavior is based on three stages of operation in a switching period, such that the power oscillating component is stored in one of the inherent zeta inductor. The theoretical foundation that justifies its operation is presented, as well as the simulation and experimental results to validate the applied concepts.
2022-02-24
Gondron, Sébastien, Mödersheim, Sebastian.  2021.  Vertical Composition and Sound Payload Abstraction for Stateful Protocols. 2021 IEEE 34th Computer Security Foundations Symposium (CSF). :1–16.
This paper deals with a problem that arises in vertical composition of protocols, i.e., when a channel protocol is used to encrypt and transport arbitrary data from an application protocol that uses the channel. Our work proves that we can verify that the channel protocol ensures its security goals independent of a particular application. More in detail, we build a general paradigm to express vertical composition of an application protocol and a channel protocol, and we give a transformation of the channel protocol where the application payload messages are replaced by abstract constants in a particular way that is feasible for standard automated verification tools. We prove that this transformation is sound for a large class of channel and application protocols. The requirements that channel and application have to satisfy for the vertical composition are all of an easy-to-check syntactic nature.
2022-04-26
Kim, Muah, Günlü, Onur, Schaefer, Rafael F..  2021.  Federated Learning with Local Differential Privacy: Trade-Offs Between Privacy, Utility, and Communication. ICASSP 2021 - 2021 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP). :2650–2654.

Federated learning (FL) allows to train a massive amount of data privately due to its decentralized structure. Stochastic gradient descent (SGD) is commonly used for FL due to its good empirical performance, but sensitive user information can still be inferred from weight updates shared during FL iterations. We consider Gaussian mechanisms to preserve local differential privacy (LDP) of user data in the FL model with SGD. The trade-offs between user privacy, global utility, and transmission rate are proved by defining appropriate metrics for FL with LDP. Compared to existing results, the query sensitivity used in LDP is defined as a variable, and a tighter privacy accounting method is applied. The proposed utility bound allows heterogeneous parameters over all users. Our bounds characterize how much utility decreases and transmission rate increases if a stronger privacy regime is targeted. Furthermore, given a target privacy level, our results guarantee a significantly larger utility and a smaller transmission rate as compared to existing privacy accounting methods.

2021-12-20
Yang, Yuhan, Zhou, Yong, Wang, Ting, Shi, Yuanming.  2021.  Reconfigurable Intelligent Surface Assisted Federated Learning with Privacy Guarantee. 2021 IEEE International Conference on Communications Workshops (ICC Workshops). :1–6.
In this paper, we consider a wireless federated learning (FL) system concerning differential privacy (DP) guarantee, where multiple edge devices collaboratively train a shared model under the coordination of a central base station (BS) through over-the-air computation (AirComp). However, due to the heterogeneity of wireless links, it is difficult to achieve the optimal trade-off between model privacy and accuracy during the FL model aggregation. To address this issue, we propose to utilize the reconfigurable intelligent surface (RIS) technology to mitigate the communication bottleneck in FL by reconfiguring the wireless propagation environment. Specifically, we aim to minimize the model optimality gap while strictly meeting the DP and transmit power constraints. This is achieved by jointly optimizing the device transmit power, artificial noise, and phase shifts at RIS, followed by developing a two-step alternating minimization framework. Simulation results will demonstrate that the proposed RIS-assisted FL model achieves a better trade-off between accuracy and privacy than the benchmarks.
2022-01-25
Sureshkumar, S, Agash, C P, Ramya, S, Kaviyaraj, R, Elanchezhiyan, S.  2021.  Augmented Reality with Internet of Things. 2021 International Conference on Artificial Intelligence and Smart Systems (ICAIS). :1426—1430.
Today technological changes make the probability of more complex things made into simple tasks with more accuracy in major areas and mostly in Manufacturing Industry. Internet of things contributes its major part in automation which helps human to make life easy by monitoring and directed to a related person with in a fraction of second. Continuous advances and improvement in computer vision, mobile computing and tablet screens have led to a revived interest in Augmented Reality the Augmented Reality makes the complex automation into an easier task by making more realistic real time animation in monitoring and automation on Internet of Things (eg like temperature, time, object information, installation manual, real time testing).In order to identify and link the augmented content, like object control of home appliances, industrial appliances. The AR-IoT will have a much cozier atmosphere and enhance the overall Interactivity of the IoT environment. Augmented Reality applications use a myriad of data generated by IoT devices and components, AR helps workers become more competitive and productive with the realistic environment in IoT. Augmented Reality and Internet of Things together plays a critical role in the development of next generation technologies. This paper describes the concept of how Augmented Reality can be integrated with industry(AR-IoT)4.0 and how the sensors are used to monitoring objects/things contiguously round the clock, and make the process of converting real-time physical objects into smart things for the upcoming new era with AR-IoT.
2022-02-09
Abi Sen, Adnan Ahmed, M Alawfi, Ibrahim Moeed, Aloufi, Hazim Faisal, Bahbouh, Nour Mahmoud, Alsaawy, Yazed.  2021.  Comparison among Cooperation, Anonymity and Cloak Area Approaches for Preserving Privacy of IoT. 2021 8th International Conference on Computing for Sustainable Global Development (INDIACom). :413–416.
As a result of the importance of privacy at present, especially with the modern applications and technologies that have spread in the last decade, many techniques and methods have appeared to preserve privacy and protect users' data from tracking, profiling, or identification. The most popular of these technologies are those which rely on peer-to-peer or third-party cooperation. But, by reviewing a significant portion of existing research articles related to privacy, we find considerable confusion amongst several concepts and ways of protection, such as the concept of cloak area, Anonymizer, cooperation, and Third Party Peers (TTP). In this research, we revisit and review these approaches, which contain an overlap between them to distinguish each one clearly with the help of graphs and to remove their ambiguity. In this way, we shall be able provide a ready-reckoner to those interested in this field to easily differentiate between them and thus work to develop them and provide new methods. In other words, this research seeks to enhance the privacy and security in smart applications and technologies in the IoT and smart city environments.
2022-01-25
Meyer, Fabian, Gehrke, Christian, Schäfer, Michael.  2021.  Evaluating User Acceptance using WebXR for an Augmented Reality Information System. 2021 IEEE Conference on Virtual Reality and 3D User Interfaces Abstracts and Workshops (VRW). :418—419.
Augmented Reality has a long history and has seen major technical advantages in the last years. With WebXR, a new web standard, Mobile Augmented Reality (MAR) applications are now available in the web browser. With our work, we implemented an Augmented Reality Information System and conducted a case study to evaluate the user acceptance of such an application build with WebXR. Our results indicate that the user acceptance regarding web-based MAR applications for our specific use case seems to be given. With our proposed architecture we also lay the foundation for other AR information systems.
2022-04-26
Kühtreiber, Patrick, Reinhardt, Delphine.  2021.  Usable Differential Privacy for the Internet-of-Things. 2021 IEEE International Conference on Pervasive Computing and Communications Workshops and other Affiliated Events (PerCom Workshops). :426–427.

Current implementations of Differential Privacy (DP) focus primarily on the privacy of the data release. The planned thesis will investigate steps towards a user-centric approach of DP in the scope of the Internet-of-Things (IoT) which focuses on data subjects, IoT developers, and data analysts. We will conduct user studies to find out more about the often conflicting interests of the involved parties and the encountered challenges. Furthermore, a technical solution will be developed to assist data subjects and analysts in making better informed decisions. As a result, we expect our contributions to be a step towards the development of usable DP for IoT sensor data.

2022-02-07
Catak, Evren, Catak, Ferhat Ozgur, Moldsvor, Arild.  2021.  Adversarial Machine Learning Security Problems for 6G: mmWave Beam Prediction Use-Case. 2021 IEEE International Black Sea Conference on Communications and Networking (BlackSeaCom). :1–6.
6G is the next generation for the communication systems. In recent years, machine learning algorithms have been applied widely in various fields such as health, transportation, and the autonomous car. The predictive algorithms will be used in 6G problems. With the rapid developments of deep learning techniques, it is critical to take the security concern into account when applying the algorithms. While machine learning offers significant advantages for 6G, AI models’ security is normally ignored. Due to the many applications in the real world, security is a vital part of the algorithms. This paper proposes a mitigation method for adversarial attacks against proposed 6G machine learning models for the millimeter-wave (mmWave) beam prediction using adversarial learning. The main idea behind adversarial attacks against machine learning models is to produce faulty results by manipulating trained deep learning models for 6G applications for mmWave beam prediction. We also present the adversarial learning mitigation method’s performance for 6G security in millimeter-wave beam prediction application with fast gradient sign method attack. The mean square errors of the defended model under attack are very close to the undefended model without attack.
2022-10-12
Sharevski, Filipo, Jachim, Peter.  2021.  Alexa in Phishingland: Empirical Assessment of Susceptibility to Phishing Pretexting in Voice Assistant Environments. 2021 IEEE Security and Privacy Workshops (SPW). :207—213.
This paper investigates what cues people use to spot a phishing email when the email is spoken back to them by the Alexa voice assistant, instead of read on a screen. We configured Alexa to read there emails to a sample of 52 participants and ask for their phishing evaluations. We also asked a control group of another 52 participants to evaluate these emails on a regular screen to compare the plausibility of phishing pretexting in voice assistant environments. The results suggest that Alexa can be used for pretexting users that lack phishing awareness to receive and act upon a relatively urgent email from an authoritative sender. Inspecting the sender (authority cue”) and relying on their personal experiences helped participants with higher phishing awareness to use Alexa towards a preliminary email screening to flag an email as potentially “phishing.”
2022-08-12
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.
2022-02-24
Lin, Junxiong, Xu, Yajing, Lu, Zhihui, Wu, Jie, Ye, Houhao, Huang, Wenbing, Chen, Xuzhao.  2021.  A Blockchain-Based Evidential and Secure Bulk-Commodity Supervisory System. 2021 International Conference on Service Science (ICSS). :1–6.
In recent years, the commodities industry has grown rapidly under the stimulus of domestic demand and the expansion of cross-border trade. It has also been combined with the rapid development of e-commerce technology in the same period to form a flexible and efficient e-commerce system for bulk commodities. However, the hasty combination of both has inspired a lack of effective regulatory measures in the bulk industry, leading to constant industry chaos. Among them, the problem of lagging evidence in regulatory platforms is particularly prominent. Based on this, we design a blockchain-based evidential and secure bulk-commodity supervisory system (abbr. BeBus). Setting different privacy protection policies for each participant in the system, the solution ensures effective forensics and tamper-proof evidence to meet the needs of the bulk business scenario.
2022-02-25
Cremers, Cas, Düzlü, Samed, Fiedler, Rune, Fischlin, Marc, Janson, Christian.  2021.  BUFFing signature schemes beyond unforgeability and the case of post-quantum signatures. 2021 IEEE Symposium on Security and Privacy (SP). :1696–1714.
Modern digital signature schemes can provide more guarantees than the standard notion of (strong) unforgeability, such as offering security even in the presence of maliciously generated keys, or requiring to know a message to produce a signature for it. The use of signature schemes that lack these properties has previously enabled attacks on real-world protocols. In this work we revisit several of these notions beyond unforgeability, establish relations among them, provide the first formal definition of non re-signability, and a transformation that can provide these properties for a given signature scheme in a provable and efficient way.Our results are not only relevant for established schemes: for example, the ongoing NIST PQC competition towards standardizing post-quantum signature schemes has six finalists in its third round. We perform an in-depth analysis of the candidates with respect to their security properties beyond unforgeability. We show that many of them do not yet offer these stronger guarantees, which implies that the security guarantees of these post-quantum schemes are not strictly stronger than, but instead incomparable to, classical signature schemes. We show how applying our transformation would efficiently solve this, paving the way for the standardized schemes to provide these additional guarantees and thereby making them harder to misuse.
2022-08-26
Frumin, Dan, Krebbers, Robbert, Birkedal, Lars.  2021.  Compositional Non-Interference for Fine-Grained Concurrent Programs. 2021 IEEE Symposium on Security and Privacy (SP). :1416—1433.
Non-interference is a program property that ensures the absence of information leaks. In the context of programming languages, there exist two common approaches for establishing non-interference: type systems and program logics. Type systems provide strong automation (by means of type checking), but they are inherently restrictive in the kind of programs they support. Program logics support challenging programs, but they typically require significant human assistance, and cannot handle modules or higher-order programs.To connect these two approaches, we present SeLoC—a separation logic for non-interference, on top of which we build a type system using the technique of logical relations. By building a type system on top of separation logic, we can compositionally verify programs that consist of typed and untyped parts. The former parts are verified through type checking, while the latter parts are verified through manual proof.The core technical contribution of SeLoC is a relational form of weakest preconditions that can track information flow using separation logic resources. SeLoC is fully machine-checked, and built on top of the Iris framework for concurrent separation logic in Coq. The integration with Iris provides seamless support for fine-grained concurrency, which was beyond the reach of prior type systems and program logics for non-interference.
2022-02-04
Cervini, James, Rubin, Aviel, Watkins, Lanier.  2021.  A Containerization-Based Backfit Approach for Industrial Control System Resiliency. 2021 IEEE Security and Privacy Workshops (SPW). :246–252.
Many industrial control systems (ICS) are reliant upon programmable logic controllers (PLCs) for their operations. As ICS and PLCs are increasingly targeted by cyber-attacks, research facilitating the resiliency of their physical processes is imperative. This paper proposes an approach which leverages PLC containerization, input/output (I/O) multiplexing, and orchestration to respond to cyber incidents and ensure continuity of critical processes. A proofof-concept capability was developed and evaluated on live ICS testbed environments. The experimental results indicate the approach is viable for control applications with soft real-time requirements.
2021-12-20
Piccolboni, Luca, Guglielmo, Giuseppe Di, Carloni, Luca P., Sethumadhavan, Simha.  2021.  CRYLOGGER: Detecting Crypto Misuses Dynamically. 2021 IEEE Symposium on Security and Privacy (SP). :1972–1989.
Cryptographic (crypto) algorithms are the essential ingredients of all secure systems: crypto hash functions and encryption algorithms, for example, can guarantee properties such as integrity and confidentiality. Developers, however, can misuse the application programming interfaces (API) of such algorithms by using constant keys and weak passwords. This paper presents CRYLOGGER, the first open-source tool to detect crypto misuses dynamically. CRYLOGGER logs the parameters that are passed to the crypto APIs during the execution and checks their legitimacy offline by using a list of crypto rules. We compared CRYLOGGER with CryptoGuard, one of the most effective static tools to detect crypto misuses. We show that our tool complements the results of CryptoGuard, making the case for combining static and dynamic approaches. We analyzed 1780 popular Android apps downloaded from the Google Play Store to show that CRYLOGGER can detect crypto misuses on thousands of apps dynamically and automatically. We reverse-engineered 28 Android apps and confirmed the issues flagged by CRYLOGGER. We also disclosed the most critical vulnerabilities to app developers and collected their feedback.