Visible to the public Biblio

Found 2348 results

Filters: Keyword is privacy  [Clear All Filters]
2020-04-20
Hu, Boyang, Yan, Qiben, Zheng, Yao.  2018.  Tracking location privacy leakage of mobile ad networks at scale. IEEE INFOCOM 2018 - IEEE Conference on Computer Communications Workshops (INFOCOM WKSHPS). :1–2.
The online advertising ecosystem is built upon the massive data collection of ad networks to learn the properties of users for targeted ad deliveries. Existing efforts have investigated the privacy leakage behaviors of mobile ad networks. However, there lacks a large-scale measurement study to evaluate the scale of privacy leakage through mobile ads. In this work, we present a study of the potential privacy leakage in location-based mobile advertising services based on a large-scale measurement. We first introduce a threat model in the mobile ad ecosystem, and then design a measurement system to perform extensive threat measurements and assessments. To counteract the privacy leakage threats, we design and implement an adaptive location obfuscation mechanism, which can be used to obfuscate location data in real-time while minimizing the impact to mobile ad businesses.
Hu, Boyang, Yan, Qiben, Zheng, Yao.  2018.  Tracking location privacy leakage of mobile ad networks at scale. IEEE INFOCOM 2018 - IEEE Conference on Computer Communications Workshops (INFOCOM WKSHPS). :1–2.
The online advertising ecosystem is built upon the massive data collection of ad networks to learn the properties of users for targeted ad deliveries. Existing efforts have investigated the privacy leakage behaviors of mobile ad networks. However, there lacks a large-scale measurement study to evaluate the scale of privacy leakage through mobile ads. In this work, we present a study of the potential privacy leakage in location-based mobile advertising services based on a large-scale measurement. We first introduce a threat model in the mobile ad ecosystem, and then design a measurement system to perform extensive threat measurements and assessments. To counteract the privacy leakage threats, we design and implement an adaptive location obfuscation mechanism, which can be used to obfuscate location data in real-time while minimizing the impact to mobile ad businesses.
Esquivel-Quiros, Luis Gustavo, Barrantes, Elena Gabriela, Darlington, Fernando Esponda.  2018.  Measuring data privacy preserving and machine learning. 2018 7th International Conference On Software Process Improvement (CIMPS). :85–94.

The increasing publication of large amounts of data, theoretically anonymous, can lead to a number of attacks on the privacy of people. The publication of sensitive data without exposing the data owners is generally not part of the software developers concerns. The regulations for the data privacy-preserving create an appropriate scenario to focus on privacy from the perspective of the use or data exploration that takes place in an organization. The increasing number of sanctions for privacy violations motivates the systematic comparison of three known machine learning algorithms in order to measure the usefulness of the data privacy preserving. The scope of the evaluation is extended by comparing them with a known privacy preservation metric. Different parameter scenarios and privacy levels are used. The use of publicly available implementations, the presentation of the methodology, explanation of the experiments and the analysis allow providing a framework of work on the problem of the preservation of privacy. Problems are shown in the measurement of the usefulness of the data and its relationship with the privacy preserving. The findings motivate the need to create optimized metrics on the privacy preferences of the owners of the data since the risks of predicting sensitive attributes by means of machine learning techniques are not usually eliminated. In addition, it is shown that there may be a hundred percent, but it cannot be measured. As well as ensuring adequate performance of machine learning models that are of interest to the organization that data publisher.

2020-04-17
Nair, Harsha, Sridaran, R..  2019.  An Innovative Model (HS) to Enhance the Security in Windows Operating System - A Case Study. 2019 6th International Conference on Computing for Sustainable Global Development (INDIACom). :1207—1211.

Confidentiality, authentication, privacy and integrity are the pillars of securing data. The most generic way of providing security is setting up passwords and usernames collectively known as login credentials. Operating systems use different techniques to ensure security of login credentials yet brute force attacks and dictionary attacks along with various other types which leads to success in passing or cracking passwords.The objective of proposed HS model is to enhance the protection of SAM file used by Windows Registry so that the system is preserved from intruders.

Mohsen, Fadi, Jafaarian, Haadi.  2019.  Raising the Bar Really High: An MTD Approach to Protect Data in Embedded Browsers. 2019 IEEE 43rd Annual Computer Software and Applications Conference (COMPSAC). 1:786—794.
The safety of web browsers is essential to the privacy of Internet users and the security of their computing systems. In the last few years, there have been several cyber attacks geared towards compromising surfers' data and systems via exploiting browser-based vulnerabilities. Android and a number of mobile operating systems have been supporting a UI component called WebView, which can be embedded in any mobile application to render the web contents. Yet, this mini-browser component has been found to be vulnerable to various kinds of attacks. For instance, an attacker in her WebView-Embedded app can inject malicious JavaScripts into the WebView to modify the web contents or to steal user's input values. This kind of attack is particularly challenging due to the full control of attackers over the content of the loaded pages. In this paper, we are proposing and testing a server-side moving target defense technique to counter the risk of JavaScript injection attacks on mobile WebViews. The solution entails creating redundant HTML forms, randomizing their attributes and values, and asserting stealthy prompts for the user data. The solution does not dictate any changes to the browser or applications codes, neither it requires key sharing with benign clients. The results of our performance and security analysis suggest that our proposed approach protects the confidentiality and integrity of user input values with minimum overhead.
Islam, Md. Jahidul, Mahin, Md., Roy, Shanto, Debnath, Biplab Chandra, Khatun, Ayesha.  2019.  DistBlackNet: A Distributed Secure Black SDN-IoT Architecture with NFV Implementation for Smart Cities. 2019 International Conference on Electrical, Computer and Communication Engineering (ECCE). :1—6.

Internet of Things (IoT) is a key emerging technology which aims to connect objects over the internet. Software Defined Networking (SDN) is another new intelligent technology within networking domain which increases the network performance and provides better security, reliability, and privacy using dynamic software programs. In this paper, we have proposed a distributed secure Black SDN-IoT architecture with NFV implementation for smart cities. We have incorporated Black SDN that is highly secured SDN which gives better result in network performances, security, and privacy and secures both metadata and payload within each layer. This architecture also tried to introduce an approach which is more effective for building a cluster by means of Black SDN. Black SDN-loT with NFV concept brings benefits to the related fields in terms of energy savings and load balancing. Moreover, Multiple distributed controller have proposed to improve availability, integrity, privacy, confidentiality and etc. In the proposed architecture, the Black network provides higher security of each network layer comparative to the conventional network. Finally, this paper has discussed the architectural design of distributed secure Black SDN-IoT with NFV for smart cities and research challenges.

Chen, Guangxuan, Wu, Di, Chen, Guangxiao, Qin, Panke, Zhang, Lei, Liu, Qiang.  2019.  Research on Digital Forensics Framework for Malicious Behavior in Cloud. 2019 IEEE 4th Advanced Information Technology, Electronic and Automation Control Conference (IAEAC). 1:1375—1379.

The difficult of detecting, response, tracing the malicious behavior in cloud has brought great challenges to the law enforcement in combating cybercrimes. This paper presents a malicious behavior oriented framework of detection, emergency response, traceability, and digital forensics in cloud environment. A cloud-based malicious behavior detection mechanism based on SDN is constructed, which implements full-traffic flow detection technology and malicious virtual machine detection based on memory analysis. The emergency response and traceability module can clarify the types of the malicious behavior and the impacts of the events, and locate the source of the event. The key nodes and paths of the infection topology or propagation path of the malicious behavior will be located security measure will be dispatched timely. The proposed IaaS service based forensics module realized the virtualization facility memory evidence extraction and analysis techniques, which can solve volatile data loss problems that often happened in traditional forensic methods.

Jmila, Houda, Blanc, Gregory.  2019.  Designing Security-Aware Service Requests for NFV-Enabled Networks. 2019 28th International Conference on Computer Communication and Networks (ICCCN). :1—9.

Network Function Virtualization (NFV) is a recent concept where virtualization enables the shift from network functions (e.g., routers, switches, load-balancers, proxies) on specialized hardware appliances to software images running on all-purpose, high-volume servers. The resource allocation problem in the NFV environment has received considerable attention in the past years. However, little attention was paid to the security aspects of the problem in spite of the increasing number of vulnerabilities faced by cloud-based applications. Securing the services is an urgent need to completely benefit from the advantages offered by NFV. In this paper, we show how a network service request, composed of a set of service function chains (SFC) should be modified and enriched to take into consideration the security requirements of the supported service. We examine the well-known security best practices and propose a two-step algorithm that extends the initial SFC requests to a more complex chaining model that includes the security requirements of the service.

You, Ruibang, Yuan, Zimu, Tu, Bibo, Cheng, Jie.  2019.  HP-SDDAN: High-Performance Software-Defined Data Access Network. 2019 IEEE 21st International Conference on High Performance Computing and Communications; IEEE 17th International Conference on Smart City; IEEE 5th International Conference on Data Science and Systems (HPCC/SmartCity/DSS). :849—856.

Recently, data protection has become increasingly important in cloud environments. The cloud platform has global user information, rich storage resource allocation information, and a fuller understanding of data attributes. At the same time, there is an urgent need for data access control to provide data security, and software-defined network, as a ready-made facility, has a global network view, global network management capabilities, and programable network rules. In this paper, we present an approach, named High-Performance Software-Defined Data Access Network (HP-SDDAN), providing software-defined data access network architecture, global data attribute management and attribute-based data access network. HP-SDDAN combines the excellent features of cloud platform and software-defined network, and fully considers the performance to implement software-defined data access network. In evaluation, we verify the effectiveness and efficiency of HP-SDDAN implementation, with only 1.46% overhead to achieve attribute-based data access control of attribute-based differential privacy.

Brugman, Jonathon, Khan, Mohammed, Kasera, Sneha, Parvania, Masood.  2019.  Cloud Based Intrusion Detection and Prevention System for Industrial Control Systems Using Software Defined Networking. 2019 Resilience Week (RWS). 1:98—104.

Industrial control systems (ICS) are becoming more integral to modern life as they are being integrated into critical infrastructure. These systems typically lack application layer encryption and the placement of common network intrusion services have large blind spots. We propose the novel architecture, Cloud Based Intrusion Detection and Prevention System (CB-IDPS), to detect and prevent threats in ICS networks by using software defined networking (SDN) to route traffic to the cloud for inspection using network function virtualization (NFV) and service function chaining. CB-IDPS uses Amazon Web Services to create a virtual private cloud for packet inspection. The CB-IDPS framework is designed with considerations to the ICS delay constraints, dynamic traffic routing, scalability, resilience, and visibility. CB-IDPS is presented in the context of a micro grid energy management system as the test case to prove that the latency of CB-IDPS is within acceptable delay thresholds. The implementation of CB-IDPS uses the OpenDaylight software for the SDN controller and commonly used network security tools such as Zeek and Snort. To our knowledge, this is the first attempt at using NFV in an ICS context for network security.

Go, Sharleen Joy Y., Guinto, Richard, Festin, Cedric Angelo M., Austria, Isabel, Ocampo, Roel, Tan, Wilson M..  2019.  An SDN/NFV-Enabled Architecture for Detecting Personally Identifiable Information Leaks on Network Traffic. 2019 Eleventh International Conference on Ubiquitous and Future Networks (ICUFN). :306—311.

The widespread adoption of social networking and cloud computing has transformed today's Internet to a trove of personal information. As a consequence, data breaches are expected to increase in gravity and occurrence. To counteract unintended data disclosure, a great deal of effort has been dedicated in devising methods for uncovering privacy leaks. Existing solutions, however, have not addressed the time- and data-intensive nature of leak detection. The shift from hardware-specific implementation to software-based solutions is the core idea behind the concept of Network Function Virtualization (NFV). On the other hand, the Software Defined Networking (SDN) paradigm is characterized by the decoupling of the forwarding and control planes. In this paper, an SDN/NFV-enabled architecture is proposed for improving the efficiency of leak detection systems. Employing a previously developed identification strategy, Personally Identifiable Information detector (PIID) and load balancer VNFs are packaged and deployed in OpenStack through an NFV MANO. Meanwhile, SDN controllers permit the load balancer to dynamically redistribute traffic among the PIID instances. In a physical testbed, tests are conducted to evaluate the proposed architecture. Experimental results indicate that the proportions of forwarding and parsing on total overhead is influenced by the traffic intensity. Furthermore, an NFV-enabled system with scalability features was found to outperform a non-virtualized implementation in terms of latency (85.1%), packet loss (98.3%) and throughput (8.41%).

Huang, Hua, Zhang, Yi-lai, Zhang, Min.  2019.  Research on Cloud Workflow Engine Supporting Three-Level Isolation and Privacy Protection. 2019 IEEE 5th Intl Conference on Big Data Security on Cloud (BigDataSecurity), IEEE Intl Conference on High Performance and Smart Computing, (HPSC) and IEEE Intl Conference on Intelligent Data and Security (IDS). :160—165.

With the development of cloud computing, cloud workflow systems are widely accepted by more and more enterprises and individuals (namely tenants). There exists mass tenant workflow instances running in cloud workflow systems. How to implement the three-level (i.e., data, performance, execution ) isolation and privacy protection among these tenant workflow instances is challenging. To address this issue, this paper presents a novel cloud workflow model supporting multi-tenants with privacy protection. With the presented model, a framework of cloud workflow engine based on the extended jBPM4 is proposed by adopting layered management thought, virtualization technology and sandbox mechanism. By extending the jBPM4 (java Business Process Management) engine, the prototype system of the proposed cloud workflow engine is implemented and applied in the ceramic cloud service platform (denoted as CCSP). The application effect demonstrates that our proposal can be used to implement the three-level isolation and privacy protection between mass various tenant workflow instances in cloud workflow systems.

Yang, Zihan, Mi, Zeyu, Xia, Yubin.  2019.  Undertow: An Intra-Kernel Isolation Mechanism for Hardware-Assisted Virtual Machines. 2019 IEEE International Conference on Service-Oriented System Engineering (SOSE). :257—2575.
The prevalence of Cloud Computing has appealed many users to put their business into low-cost and flexible cloud servers instead of bare-metal machines. Most virtual machines in the cloud run commodity operating system(e.g., linux), and the complexity of such operating systems makes them more bug-prone and easier to be compromised. To mitigate the security threats, previous works attempt to mediate and filter system calls, transform all unpopular paths into popular paths, or implement a nested kernel along with the untrusted outter kernel to enforce certain security policies. However, such solutions only enforce read-only protection or assume that popular paths in the kernel to contain almost no bug, which is not always the case in the real world. To overcome their shortcomings and combine their advantages as much as possible, we propose a hardware-assisted isolation mechanism that isolates untrusted part of the kernel. To achieve isolation, we prepare multiple restricted Extended Page Table (EPT) during boot time, each of which has certain critical data unmapped from it so that the code executing in the isolated environment could not access sensitive data. We leverage the VMFUNC instruction already available in recent Intel processors to directly switch to another pre-defined EPT inside guest virtual machine without trapping into the underlying hypervisor, which is faster than the traditional trap-and-emulate procedure. The semantic gap is minimized and real-time check is achieved by allowing EPT violations to be converted to Virtualization Exception (VE), which could be handled inside guest kernel in non-root mode. Our preliminary evaluation shows that with hardware virtualization feature, we are able to run the untrusted code in an isolated environment with negligible overhead.
Liu, Sihang, Wei, Yizhou, Chi, Jianfeng, Shezan, Faysal Hossain, Tian, Yuan.  2019.  Side Channel Attacks in Computation Offloading Systems with GPU Virtualization. 2019 IEEE Security and Privacy Workshops (SPW). :156—161.

The Internet of Things (IoT) and mobile systems nowadays are required to perform more intensive computation, such as facial detection, image recognition and even remote gaming, etc. Due to the limited computation performance and power budget, it is sometimes impossible to perform these workloads locally. As high-performance GPUs become more common in the cloud, offloading the computation to the cloud becomes a possible choice. However, due to the fact that offloaded workloads from different devices (belonging to different users) are being computed in the same cloud, security concerns arise. Side channel attacks on GPU systems have been widely studied, where the threat model is the attacker and the victim are running on the same operating system. Recently, major GPU vendors have provided hardware and library support to virtualize GPUs for better isolation among users. This work studies the side channel attacks from one virtual machine to another where both share the same physical GPU. We show that it is possible to infer other user's activities in this setup and can further steal others deep learning model.

2020-04-13
Mohanta, Bhabendu K., Panda, Soumyashree S., Satapathy, Utkalika, Jena, Debasish, Gountia, Debasis.  2019.  Trustworthy Management in Decentralized IoT Application using Blockchain. 2019 10th International Conference on Computing, Communication and Networking Technologies (ICCCNT). :1–5.
Internet of Things (IoT) as per estimated will connect 50 billion devices by 2020. Since its evolution, IoT technology provides lots of flexibility to develop and implement any application. Most of the application improves the human living standard and also makes life easy to access and monitoring the things in real time. Though there exist some security and privacy issues in IoT system like authentication, computation, data modification, trust among users. In this paper, we have identified the IoT application like insurance, supply chain system, smart city and smart car where trust among associated users is an major issue. The current centralized system does not provide enough trust between users. Using Blockchain technology we have shown that trust issue among users can be managed in a decentralized way so that information can be traceable and identify/verify any time. Blockchain has properties like distributed, digitally share and immutable which enhance security. For Blockchain implementation, Ethereum platform is used.
Grissa, Mohamed, Yavuz, Attila A., Hamdaoui, Bechir.  2019.  TrustSAS: A Trustworthy Spectrum Access System for the 3.5 GHz CBRS Band. IEEE INFOCOM 2019 - IEEE Conference on Computer Communications. :1495–1503.
As part of its ongoing efforts to meet the increased spectrum demand, the Federal Communications Commission (FCC) has recently opened up 150 MHz in the 3.5 GHz band for shared wireless broadband use. Access and operations in this band, aka Citizens Broadband Radio Service (CBRS), will be managed by a dynamic spectrum access system (SAS) to enable seamless spectrum sharing between secondary users (SUs) and incumbent users. Despite its benefits, SAS's design requirements, as set by FCC, present privacy risks to SUs, merely because SUs are required to share sensitive operational information (e.g., location, identity, spectrum usage) with SAS to be able to learn about spectrum availability in their vicinity. In this paper, we propose TrustSAS, a trustworthy framework for SAS that synergizes state-of-the-art cryptographic techniques with blockchain technology in an innovative way to address these privacy issues while complying with FCC's regulatory design requirements. We analyze the security of our framework and evaluate its performance through analysis, simulation and experimentation. We show that TrustSAS can offer high security guarantees with reasonable overhead, making it an ideal solution for addressing SUs' privacy issues in an operational SAS environment.
2020-04-06
Patsonakis, Christos, Samari, Katerina, Kiayiasy, Aggelos, Roussopoulos, Mema.  2019.  On the Practicality of a Smart Contract PKI. 2019 IEEE International Conference on Decentralized Applications and Infrastructures (DAPPCON). :109–118.
Public key infrastructures (PKIs) are one of the main building blocks for securing communications over the Internet. Currently, PKIs are under the control of centralized authorities, which is problematic as evidenced by numerous incidents where they have been compromised. The distributed, fault tolerant log of transactions provided by blockchains and more recently, smart contract platforms, constitutes a powerful tool for the decentralization of PKIs. To verify the validity of identity records, blockchain-based identity systems store on chain either all identity records, or, a small (or even constant) sized amount of data for verifying identity records stored off chain. However, as most of these systems have never been implemented, there is little information regarding the practical implications of each design's tradeoffs. In this work, we first implement and evaluate the only provably secure, smart contract based PKI of Patsonakis et al. on top of Ethereum. This construction incurs constant-sized storage at the expense of computational complexity. To explore this tradeoff, we propose and implement a second construction which, eliminates the need for trusted setup, preserves the security properties of Patsonakis et al. and, as illustrated through our evaluation, is the only version with constant-sized state that can be deployed on the live chain of Ethereum. Furthermore, we compare these two systems with the simple approach of most prior works, e.g., the Ethereum Name Service, where all identity records are stored on the smart contract's state, to illustrate several shortcomings of Ethereum and its cost model. We propose several modifications for fine tuning the model, which would be useful to be considered for any smart contract platform like Ethereum so that it reaches its full potential to support arbitrary distributed applications.
2020-04-03
Song, Liwei, Shokri, Reza, Mittal, Prateek.  2019.  Membership Inference Attacks Against Adversarially Robust Deep Learning Models. 2019 IEEE Security and Privacy Workshops (SPW). :50—56.
In recent years, the research community has increasingly focused on understanding the security and privacy challenges posed by deep learning models. However, the security domain and the privacy domain have typically been considered separately. It is thus unclear whether the defense methods in one domain will have any unexpected impact on the other domain. In this paper, we take a step towards enhancing our understanding of deep learning models when the two domains are combined together. We do this by measuring the success of membership inference attacks against two state-of-the-art adversarial defense methods that mitigate evasion attacks: adversarial training and provable defense. On the one hand, membership inference attacks aim to infer an individual's participation in the target model's training dataset and are known to be correlated with target model's overfitting. On the other hand, adversarial defense methods aim to enhance the robustness of target models by ensuring that model predictions are unchanged for a small area around each sample in the training dataset. Intuitively, adversarial defenses may rely more on the training dataset and be more vulnerable to membership inference attacks. By performing empirical membership inference attacks on both adversarially robust models and corresponding undefended models, we find that the adversarial training method is indeed more susceptible to membership inference attacks, and the privacy leakage is directly correlated with model robustness. We also find that the provable defense approach does not lead to enhanced success of membership inference attacks. However, this is achieved by significantly sacrificing the accuracy of the model on benign data points, indicating that privacy, security, and prediction accuracy are not jointly achieved in these two approaches.
Zhao, Hui, Li, Zhihui, Wei, Hansheng, Shi, Jianqi, Huang, Yanhong.  2019.  SeqFuzzer: An Industrial Protocol Fuzzing Framework from a Deep Learning Perspective. 2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST). :59—67.

Industrial networks are the cornerstone of modern industrial control systems. Performing security checks of industrial communication processes helps detect unknown risks and vulnerabilities. Fuzz testing is a widely used method for performing security checks that takes advantage of automation. However, there is a big challenge to carry out security checks on industrial network due to the increasing variety and complexity of industrial communication protocols. In this case, existing approaches usually take a long time to model the protocol for generating test cases, which is labor-intensive and time-consuming. This becomes even worse when the target protocol is stateful. To help in addressing this problem, we employed a deep learning model to learn the structures of protocol frames and deal with the temporal features of stateful protocols. We propose a fuzzing framework named SeqFuzzer which automatically learns the protocol frame structures from communication traffic and generates fake but plausible messages as test cases. For proving the usability of our approach, we applied SeqFuzzer to widely-used Ethernet for Control Automation Technology (EtherCAT) devices and successfully detected several security vulnerabilities.

Lipp, Benjamin, Blanchet, Bruno, Bhargavan, Karthikeyan.  2019.  A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol. 2019 IEEE European Symposium on Security and Privacy (EuroS P). :231—246.

WireGuard is a free and open source Virtual Private Network (VPN) that aims to replace IPsec and OpenVPN. It is based on a new cryptographic protocol derived from the Noise Protocol Framework. This paper presents the first mechanised cryptographic proof of the protocol underlying WireGuard, using the CryptoVerif proof assistant. We analyse the entire WireGuard protocol as it is, including transport data messages, in an ACCE-style model. We contribute proofs for correctness, message secrecy, forward secrecy, mutual authentication, session uniqueness, and resistance against key compromise impersonation, identity mis-binding, and replay attacks. We also discuss the strength of the identity hiding provided by WireGuard. Our work also provides novel theoretical contributions that are reusable beyond WireGuard. First, we extend CryptoVerif to account for the absence of public key validation in popular Diffie-Hellman groups like Curve25519, which is used in many modern protocols including WireGuard. To our knowledge, this is the first mechanised cryptographic proof for any protocol employing such a precise model. Second, we prove several indifferentiability lemmas that are useful to simplify the proofs for sequences of key derivations.

Aires Urquiza, Abraão, AlTurki, Musab A., Kanovich, Max, Ban Kirigin, Tajana, Nigam, Vivek, Scedrov, Andre, Talcott, Carolyn.  2019.  Resource-Bounded Intruders in Denial of Service Attacks. 2019 IEEE 32nd Computer Security Foundations Symposium (CSF). :382—38214.

Denial of Service (DoS) attacks have been a serious security concern, as no service is, in principle, protected against them. Although a Dolev-Yao intruder with unlimited resources can trivially render any service unavailable, DoS attacks do not necessarily have to be carried out by such (extremely) powerful intruders. It is useful in practice and more challenging for formal protocol verification to determine whether a service is vulnerable even to resource-bounded intruders that cannot generate or intercept arbitrary large volumes of traffic. This paper proposes a novel, more refined intruder model where the intruder can only consume at most some specified amount of resources in any given time window. Additionally, we propose protocol theories that may contain timeouts and specify service resource usage during protocol execution. In contrast to the existing resource-conscious protocol verification models, our model allows finer and more subtle analysis of DoS problems. We illustrate the power of our approach by representing a number of classes of DoS attacks, such as, Slow, Asymmetric and Amplification DoS attacks, exhausting different types of resources of the target, such as, number of workers, processing power, memory, and network bandwidth. We show that the proposed DoS problem is undecidable in general and is PSPACE-complete for the class of resource-bounded, balanced systems. Finally, we implemented our formal verification model in the rewriting logic tool Maude and analyzed a number of DoS attacks in Maude using Rewriting Modulo SMT in an automated fashion.

Nandi, Giann Spilere, Pereira, David, Vigil, Martín, Moraes, Ricardo, Morales, Analúcia Schiaffino, Araújo, Gustavo.  2019.  Security in Wireless Sensor Networks: A formal verification of protocols. 2019 IEEE 17th International Conference on Industrial Informatics (INDIN). 1:425—431.

The increase of the digitalization taking place in various industrial domains is leading developers towards the design and implementation of more and more complex networked control systems (NCS) supported by Wireless Sensor Networks (WSN). This naturally raises new challenges for the current WSN technology, namely in what concerns improved guarantees of technical aspects such as real-time communications together with safe and secure transmissions. Notably, in what concerns security aspects, several cryptographic protocols have been proposed. Since the design of these protocols is usually error-prone, security breaches can still be exposed and MALICIOUSly exploited unless they are rigorously analyzed and verified. In this paper we formally verify, using ProVerif, three cryptographic protocols used in WSN, regarding the security properties of secrecy and authenticity. The security analysis performed in this paper is more robust than the ones performed in related work. Our contributions involve analyzing protocols that were modeled considering an unbounded number of participants and actions, and also the use of a hierarchical system to classify the authenticity results. Our verification shows that the three analyzed protocols guarantee secrecy, but can only provide authenticity in specific scenarios.

Fattahi, Jaouhar, Mejri, Mohamed, Pricop, Emil.  2019.  On the Security of Cryptographic Protocols Using the Little Theorem of Witness Functions. 2019 IEEE Canadian Conference of Electrical and Computer Engineering (CCECE). :1—5.

In this paper, we show how practical the little theorem of witness functions is in detecting security flaws in some categories of cryptographic protocols. We convey a formal analysis of the Needham-Schroeder symmetric-key protocol in the theory of witness functions. We show how it helps to warn about a security vulnerability in a given step of this protocol where the value of security of a sensitive ticket in a sent message unexpectedly decreases compared with its value when received. This vulnerability may be exploited by an intruder to mount a replay attack as described by Denning and Sacco.

Künnemann, Robert, Esiyok, Ilkan, Backes, Michael.  2019.  Automated Verification of Accountability in Security Protocols. 2019 IEEE 32nd Computer Security Foundations Symposium (CSF). :397—39716.

Accountability is a recent paradigm in security protocol design which aims to eliminate traditional trust assumptions on parties and hold them accountable for their misbehavior. It is meant to establish trust in the first place and to recognize and react if this trust is violated. In this work, we discuss a protocol-agnostic definition of accountability: a protocol provides accountability (w.r.t. some security property) if it can identify all misbehaving parties, where misbehavior is defined as a deviation from the protocol that causes a security violation. We provide a mechanized method for the verification of accountability and demonstrate its use for verification and attack finding on various examples from the accountability and causality literature, including Certificate Transparency and Krollˆ\textbackslashtextbackslashprimes Accountable Algorithms protocol. We reach a high degree of automation by expressing accountability in terms of a set of trace properties and show their soundness and completeness.

Fawaz, Kassem, Linden, Thomas, Harkous, Hamza.  2019.  Invited Paper: The Applications of Machine Learning in Privacy Notice and Choice. 2019 11th International Conference on Communication Systems Networks (COMSNETS). :118—124.
For more than two decades since the rise of the World Wide Web, the “Notice and Choice” framework has been the governing practice for the disclosure of online privacy practices. The emergence of new forms of user interactions, such as voice, and the enforcement of new regulations, such as the EU's recent General Data Protection Regulation (GDPR), promise to change this privacy landscape drastically. This paper discusses the challenges towards providing the privacy stakeholders with privacy awareness and control in this changing landscape. We will also present our recent research on utilizing Machine learning to analyze privacy policies and settings.