arXiv subjects

Mira Mezini

Publications and source records attributed to Mira Mezini.

At least 55 records · Page 3Linked to original sources

arXiv2022

CamBench -- Cryptographic API Misuse Detection Tool Benchmark Suite

Context: Cryptographic APIs are often misused in real-world applications. Therefore, many cryptographic API misuse detection tools have been introduced. However, there exists no established reference benchmark for a fair and comprehensive comparison and evaluation of these tools. While there are benchmarks, they often only address a subset of the domain or were only used to evaluate a subset of existing misuse detection tools. Objective: To fairly compare cryptographic API misuse detection tools and to drive future development in this domain, we will devise such a benchmark. Openness and transparency in the generation process are key factors to fairly generate and establish the needed benchmark. Method: We propose an approach where we derive the benchmark generation methodology from the literature which consists of general best practices in benchmarking and domain-specific benchmark generation. A part of this methodology is transparency and openness of the generation process, which is achieved by pre-registering this work. Based on our methodology we design CamBench, a fair "Cryptographic API Misuse Detection Tool Benchmark Suite". We will implement the first version of CamBench limiting the domain to Java, the JCA, and static analyses. Finally, we will use CamBench to compare current misuse detection tools and compare CamBench to related benchmarks of its domain.

cs.SE↗

arXiv2021

Python Crypto Misuses in the Wild

Background: Previous studies have shown that up to 99.59 % of the Java apps using crypto APIs misuse the API at least once. However, these studies have been conducted on Java and C, while empirical studies for other languages are missing. For example, a controlled user study with crypto tasks in Python has shown that 68.5 % of the professional developers write a secure solution for a crypto task. Aims: To understand if this observation holds for real-world code, we conducted a study of crypto misuses in Python. Method: We developed a static analysis tool that covers common misuses of 5 different Python crypto APIs. With this analysis, we analyzed 895 popular Python projects from GitHub and 51 MicroPython projects for embedded devices. Further, we compared our results with the findings of previous studies. Results: Our analysis reveals that 52.26 % of the Python projects have at least one misuse. Further, some Python crypto libraries API design helps developers from misusing crypto functions, which were much more common in studies conducted with Java and C code. Conclusion: We conclude that we can see a positive impact of the good API design on crypto misuses for Python applications. Further, our analysis of MicroPython projects reveals the importance of hybrid analyses.

cs.SE↗

arXiv2021

Fex: Assisted Identification of Domain Features from C Programs

Modern software typically performs more than one functionality. These functionalities or features are not always organized in a way for modules representing these features to be used individually. Many software engineering approaches like programming language constructs, or product line visualization techniques have been proposed to organize projects as modules. Unfortunately, much legacy software suffer from years or decades of improper coding practices that leave the modules in the code almost undetectable. In such scenarios, a desirable requirement is to identify modules representing different features to be extracted. In this paper, we propose a novel approach that combines information retrieval and program analysis approaches to allow domain experts to identify slices of the program that represent modules using natural language search terms. We evaluate our approach by building a proof of concept tool in C, and extract modules from open source projects.

cs.SE↗

arXiv2021

Dealing with Variability in API Misuse Specification

APIs are the primary mechanism for developers to gain access to externally defined services and tools. However, previous research has revealed API misuses that violate the contract of APIs to be prevalent. Such misuses can have harmful consequences, especially in the context of cryptographic libraries. Various API misuse detectors have been proposed to address this issue including CogniCrypt, one of the most versatile of such detectors and that uses a language CrySL to specify cryptographic API usage contracts. Nonetheless, existing approaches to detect API misuse had not been designed for systematic reuse, ignoring the fact that different versions of a library, different versions of a platform, and different recommendations or guidelines might introduce variability in the correct usage of an API. Yet, little is known about how such variability impacts the specification of the correct API usage. This paper investigates this question by analyzing the impact of various sources of variability on widely used Java cryptographic libraries including JCA, Bouncy Castle, and Google Tink. The results of our investigation show that sources of variability like new versions of the API and security standards significantly impact the specifications. We then use the insights gained from our investigation to motivate an extension to the CrySL language named MetaCrySL, which builds on meta programming concepts. We evaluate MetaCrySL by specifying usage rules for a family of Android versions and illustrate that MetaCrySL can model all forms of variability we identified and drastically reduce the size of a family of specifications for the correct usage of cryptographic APIs

cs.CR↗

arXiv2021

ReactiFi: Reactive Programming of Wi-Fi Firmware on Mobile Devices

Network programmability will be required to handle future increased network traffic and constantly changing application needs. However, there is currently no way of using a high-level, easy to use programming language to program Wi-Fi firmware. This impedes rapid prototyping and deployment of novel network services/applications and hinders continuous performance optimization in Wi-Fi networks, since expert knowledge is required for both the used hardware platforms and the Wi-Fi domain. In this paper, we present ReactiFi, a high-level reactive programming language to program Wi-Fi chips on mobile consumer devices. ReactiFi enables programmers to implement extensions of PHY, MAC, and IP layer mechanisms without requiring expert knowledge of Wi-Fi chips, allowing for novel applications and network protocols. ReactiFi programs are executed directly on the Wi-Fi chip, improving performance and power consumption compared to execution on the main CPU. ReactiFi is conceptually similar to functional reactive languages, but is dedicated to the domain-specific needs of Wi-Fi firmware. First, it handles low-level platform-specific details without interfering with the core functionality of Wi-Fi chips. Second, it supports static reasoning about memory usage of applications, which is important for typically memory-constrained Wi-Fi chips. Third, it limits dynamic changes of dependencies between computations to dynamic branching, in order to enable static reasoning about the order of computations. We evaluate ReactiFi empirically in two real-world case studies. Our results show that throughput, latency, and power consumption are significantly improved when executing applications on the Wi-Fi chip rather than in the operating system kernel or in user space. Moreover, we show that the high-level programming abstractions of ReactiFi have no performance overhead compared to manually written C code.

cs.PL↗

arXiv2020

Mind the GAP: Security & Privacy Risks of Contact Tracing Apps

Google and Apple have jointly provided an API for exposure notification in order to implement decentralized contract tracing apps using Bluetooth Low Energy, the so-called "Google/Apple Proposal", which we abbreviate by "GAP". We demonstrate that in real-world scenarios the current GAP design is vulnerable to (i) profiling and possibly de-anonymizing infected persons, and (ii) relay-based wormhole attacks that basically can generate fake contacts with the potential of affecting the accuracy of an app-based contact tracing system. For both types of attack, we have built tools that can easily be used on mobile phones or Raspberry Pis (e.g., Bluetooth sniffers). The goal of our work is to perform a reality check towards possibly providing empirical real-world evidence for these two privacy and security risks. We hope that our findings provide valuable input for developing secure and privacy-preserving digital contact tracing systems.

cs.CR↗

arXiv2020

Uncovering the Hidden Dangers: Finding Unsafe Go Code in the Wild

The Go programming language aims to provide memory and thread safety through measures such as automated memory management with garbage collection and a strict type system. However, it also offers a way of circumventing this safety net through the use of the unsafe package. While there are legitimate use cases for unsafe, developers must exercise caution to avoid introducing vulnerabilities like buffer overflows or memory corruption in general. Using go-geiger, we conducted a study on the usage of unsafe in the top 500 most popular open-source Go projects on GitHub, including a manual analysis of 1,400 code samples on how unsafe is used. From the projects using Go's module system, 38% directly contain at least one unsafe usage, and 91% contain at least one unsafe usage in the project itself or one of its transitive dependencies. Based on the usage patterns found, we present possible exploit vectors in different scenarios. Finally, we present go-safer, a novel static analysis tool to identify dangerous and common usage patterns that were previously undetected with existing tools.

cs.CR↗

arXiv2020

Modular Collaborative Program Analysis in OPAL

Current approaches combining multiple static analyses deriving different, independent properties focus either on modularity or performance. Whereas declarative approaches facilitate modularity and automated, analysis-independent optimizations, imperative approaches foster manual, analysis-specific optimizations. In this paper, we present a novel approach to static analyses that leverages the modularity of blackboard systems and combines declarative and imperative techniques. Our approach allows exchangeability, and pluggable extension of analyses in order to improve sound(i)ness, precision, and scalability and explicitly enables the combination of otherwise incompatible analyses. With our approach integrated in the OPAL framework, we were able to implement various dissimilar analyses, including a points-to analysis that outperforms an equivalent analysis from Doop, the state-of-the-art points-to analysis framework.

cs.SE↗

arXiv2020

Hidden in Plain Sight: Obfuscated Strings Threatening Your Privacy

String obfuscation is an established technique used by proprietary, closed-source applications to protect intellectual property. Furthermore, it is also frequently used to hide spyware or malware in applications. In both cases, the techniques range from bit-manipulation over XOR operations to AES encryption. However, string obfuscation techniques/tools suffer from one shared weakness: They generally have to embed the necessary logic to deobfuscate strings into the app code. In this paper, we show that most of the string obfuscation techniques found in malicious and benign applications for Android can easily be broken in an automated fashion. We developed StringHound, an open-source tool that uses novel techniques that identify obfuscated strings and reconstruct the originals using slicing. We evaluated StringHound on both benign and malicious Android apps. In summary, we deobfuscate almost 30 times more obfuscated strings than other string deobfuscation tools. Additionally, we analyzed 100,000 Google Play Store apps and found multiple obfuscated strings that hide vulnerable cryptographic usages, insecure internet accesses, API keys, hard-coded passwords, and exploitation of privileges without the awareness of the developer. Furthermore, our analysis reveals that not only malware uses string obfuscation but also benign apps make extensive use of string obfuscation.

cs.CR↗

arXiv2019

DTN7: An Open-Source Disruption-tolerant Networking Implementation of Bundle Protocol 7

In disruption-tolerant networking (DTN), data is transmitted in a store-carry-forward fashion from network node to network node. In this paper, we present an open source DTN implementation, called DTN7, of the recently released Bundle Protocol Version 7 (draft version 13). DTN7 is written in Go and provides features like memory safety and concurrent execution. With its modular design and interchangeable components, DTN7 facilitates DTN research and application development. Furthermore, we present results of a comparative experimental evaluation of DTN7 and other DTN systems including Serval, IBR-DTN, and Forban. Our results indicate that DTN7 is a flexible and efficient open-source multi-platform implementation of the most recent Bundle Protocol Version 7.

cs.NI↗

arXiv2019

Smart Street Lights and Mobile Citizen Apps for Resilient Communication in a Digital City

Currently, nearly four billion people live in urban areas. Since this trend is increasing, natural disasters or terrorist attacks in such areas affect an increasing number of people. While information and communication technology is crucial for the operation of urban infrastructures and the well-being of its inhabitants, current technology is quite vulnerable to disruptions of various kinds. In future smart cities, a more resilient urban infrastructure is imperative to handle the increasing number of hazardous situations. We present a novel resilient communication approach based on smart street lights as part of the public infrastructure. It supports people in their everyday life and adapts its functionality to the challenges of emergency situations. Our approach relies on various environmental sensors and in-situ processing for automatic situation assessment, and a range of communication mechanisms (e.g., public WiFi hotspot functionality and mesh networking) for maintaining a communication network. Furthermore, resilience is not only achieved based on infrastructure deployed by a digital city's municipality, but also based on integrating citizens through software that runs on their mobile devices (e.g., smartphones and tablets). Web-based zero-installation and platform-agnostic apps can switch to device-to-device communication to continue benefiting people even during a disaster situation. Our approach, featuring a covert channel for professional responders and the zero-installation app, is evaluated through a prototype implementation based on a commercially available street light.

cs.HC↗

arXiv2019

Type-safe, Polyvariadic Event Correlation

The pivotal role that event correlation technology plays in todays applications has lead to the emergence of different families of event correlation approaches with a multitude of specialized correlation semantics, including computation models that support the composition and extension of different semantics. However, type-safe embeddings of extensible and composable event patterns into statically-typed general-purpose programming languages have not been systematically explored so far. Event correlation technology has often adopted well-known and intuitive notations from database queries, for which approaches to type-safe embedding do exist. However, we argue in the paper that these approaches, which are essentially descendants of the work on monadic comprehensions, are not well-suited for event correlations and, thus, cannot without further ado be reused/re-purposed for embedding event patterns. To close this gap we propose PolyJoin, a novel approach to type-safe embedding for fully polyvariadic event patterns with polymorphic correlation semantics. Our approach is based on a tagless final encoding with uncurried higher-order abstract syntax (HOAS) representation of event patterns with n variables, for arbitrary $n \in \mathbb{N}$. Thus, our embedding is defined in terms of the host language without code generation and exploits the host language type system to model and type check the type system of the pattern language. Hence, by construction it impossible to define ill-typed patterns. We show that it is possible to have a purely library-level embedding of event patterns, in the familiar join query notation, which is not restricted to monads. PolyJoin is practical, type-safe and extensible. An implementation of it in pure multicore OCaml is readily usable.

cs.PL↗

arXiv2019

How to Avoid Making a Billion-Dollar Mistake: Type-Safe Data Plane Programming with SafeP4

The P4 programming language offers high-level, declarative abstractions that bring the flexibility of software to the domain of networking. Unfortunately, the main abstraction used to represent packet data in P4, namely header types, lacks basic safety guarantees. Over the last few years, experience with an increasing number of programs has shown the risks of the unsafe approach, which often leads to subtle software bugs. This paper proposes SafeP4, a domain-specific language for programmable data planes in which all packet data is guaranteed to have a well-defined meaning and satisfy essential safety guarantees. We equip SafeP4 with a formal semantics and a static type system that statically guarantees header validity---a common source of safety bugs according to our analysis of real-world P4 programs. Statically ensuring header validity is challenging because the set of valid headers can be modified at runtime, making it a dynamic program property. Our type system achieves static safety by using a form of path-sensitive reasoning that tracks dynamic information from conditional statements, routing tables, and the control plane. Our evaluation shows that SafeP4's type system can effectively eliminate common failures in many real-world programs.

cs.PL↗

arXiv2019

Comprehensive Multiparty Session Types

Multiparty session types (MST) are a well-established type theory that describes the interactive structure of a fixed number of components from a global point of view and type-checks the components through projection of the global type onto the participants of the session. They guarantee communicationsafety for a language of multiparty sessions (LMS), i.e., distributed, parallel components can exchange values without deadlocking and unexpected message types. Several variants of MST and LMS have been proposed to study key features of distributed and parallel programming. We observe that the population of the considered variants follows from only one ancestor, i.e., the original LMS/MST, and there are overlapping traits between features of the considered variants and the original. These hamper evolution of session types and languages and their adoption in practice. This paper addresses the following question: What are the essential features for MST and LMS, and how can these be modelled with simple constructs? To the best of our knowledge, this is the first time this question has been addressed. We performed a systematic analysis of the features and the constructs in MST, LMS, and the considered variants to identify the essential features. The variants are among the most influential (according to Google Scholar) and well-established systems that cover a wide set of areas in distributed, parallel programming. We used classical techniques of formal models such as BNF, structural congruence, small step operational semantics and typing judgments to build our language and type system. Lastly, the coherence of operational semantics and type system is proven by induction. This paper proposes a set of essential features, a language of structured interactions and a type theory of comprehensive multiparty session types, including global types and type system. The analysis removes overlapping features and captures the shared traits, thereby introducing the essential features. The constructs of the language are simple and fundamental, based on the $λ$ and $π$ calculi. Analogously, our global types reflect what is omitted and introduced in the language. Our system covers all the features of the original and variants, with a better ratio of the number of language and type constructs over the number of covered features. The features of the original, variants, and our system along with the number of constructs in the respective language and global types to model them are presented through a table. The syntax, operational semantics, meta-theory and type system of our system are given. We modelled all the motivating examples of the variants in our model, describing the reduction and typing steps. The work discusses how new features, in particular the non-essential ones (formerly excluded) and advanced ones can be either modelled atop the essential ones or added with minimal efforts, i.e. without modifying the existing ones. The fundamental properties of typed processes such as subject reduction, communication safety, and progress are established.

cs.PL↗

arXiv2018

A Co-contextual Type Checker for Featherweight Java (incl. Proofs)

This paper addresses compositional and incremental type checking for object-oriented programming languages. Recent work achieved incremental type checking for structurally typed functional languages through co-contextual typing rules, a constraint-based formulation that removes any context dependency for expression typings. However, that work does not cover key features of object-oriented languages: Subtype polymorphism, nominal typing, and implementation inheritance. Type checkers encode these features in the form of class tables, an additional form of typing context inhibiting incrementalization. In the present work, we demonstrate that an appropriate co-contextual notion to class tables exists, paving the way to efficient incremental type checkers for object-oriented languages. This yields a novel formulation of Igarashi et al.'s Featherweight Java (FJ) type system, where we replace class tables by the dual concept of class table requirements and class table operations by dual operations on class table requirements. We prove the equivalence of FJ's type system and our co-contextual formulation. Based on our formulation, we implemented an incremental FJ type checker and compared its performance against javac on a number of realistic example programs.

cs.PL↗

arXiv2018

A Systematic Evaluation of Static API-Misuse Detectors

Application Programming Interfaces (APIs) often have usage constraints, such as restrictions on call order or call conditions. API misuses, i.e., violations of these constraints, may lead to software crashes, bugs, and vulnerabilities. Though researchers developed many API-misuse detectors over the last two decades, recent studies show that API misuses are still prevalent. Therefore, we need to understand the capabilities and limitations of existing detectors in order to advance the state of the art. In this paper, we present the first-ever qualitative and quantitative evaluation that compares static API-misuse detectors along the same dimensions, and with original author validation. To accomplish this, we develop MUC, a classification of API misuses, and MUBenchPipe, an automated benchmark for detector comparison, on top of our misuse dataset, MUBench. Our results show that the capabilities of existing detectors vary greatly and that existing detectors, though capable of detecting misuses, suffer from extremely low precision and recall. A systematic root-cause analysis reveals that, most importantly, detectors need to go beyond the naive assumption that a deviation from the most-frequent usage corresponds to a misuse and need to obtain additional usage examples to train their models. We present possible directions towards more-powerful API-misuse detectors.

cs.SE↗

arXiv2017

CrySL: Validating Correct Usage of Cryptographic APIs

Various studies have empirically shown that the majority of Java and Android apps misuse cryptographic libraries, causing devastating breaches of data security. Therefore, it is crucial to detect such misuses early in the development process. The fact that insecure usages are not the exception but the norm precludes approaches based on property inference and anomaly detection. In this paper, we present CrySL, a definition language that enables cryptography experts to specify the secure usage of the cryptographic libraries that they provide. CrySL combines the generic concepts of method-call sequences and data-flow constraints with domain-specific constraints related to cryptographic algorithms and their parameters. We have implemented a compiler that translates a CrySL ruleset into a context- and flow-sensitive demand-driven static analysis. The analysis automatically checks a given Java or Android app for violations of the CrySL-encoded rules. We empirically evaluated our ruleset through analyzing 10,001 Android apps. Our results show that misuse of cryptographic APIs is still widespread, with 96% of apps containing at least one misuse. However, we observed fewer of the misuses that were reported in previous work.

cs.SE↗

arXiv2016

CPL: A Core Language for Cloud Computing -- Technical Report

Running distributed applications in the cloud involves deployment. That is, distribution and configuration of application services and middleware infrastructure. The considerable complexity of these tasks resulted in the emergence of declarative JSON-based domain-specific deployment languages to develop deployment programs. However, existing deployment programs unsafely compose artifacts written in different languages, leading to bugs that are hard to detect before run time. Furthermore, deployment languages do not provide extension points for custom implementations of existing cloud services such as application-specific load balancing policies. To address these shortcomings, we propose CPL (Cloud Platform Language), a statically-typed core language for programming both distributed applications as well as their deployment on a cloud platform. In CPL, application services and deployment programs interact through statically typed, extensible interfaces, and an application can trigger further deployment at run time. We provide a formal semantics of CPL and demonstrate that it enables type-safe, composable and extensible libraries of service combinators, such as load balancing and fault tolerance.

cs.PL↗