arXiv subjects

Aslan Askarov

Publications and source records attributed to Aslan Askarov.

9 recordsLinked to original sources

arXiv2025

The downgrading semantics of memory safety (Extended version)

Memory safety is traditionally characterized in terms of bad things that cannot happen. This approach is currently embraced in the literature on formal methods for memory safety. However, a general semantic principle for memory safety, that implies the negative items, remains elusive. This paper focuses on the allocator-specific aspects of memory safety, such as null-pointer dereference, use after free, double free, and heap overflow. To that extent, we propose a notion of gradual allocator independence that accurately captures the allocator-dependent aspects of memory safety. Our approach is inspired by the previously suggested connection between memory safety and noninterference, but extends that connection in a fundamentally important direction towards downgrading. We consider a low-level language with access to an allocator that provides malloc and free primitives in a flat memory model. Pointers are just integers, and as such it is trivial to write memory-unsafe programs. The basic intuition of gradual allocator independence is that of noninterference, namely that allocators must not influence program execution. This intuition is refined in two important ways that account for the allocators running out-of-memory and for programs to have pointer-to-integer casts. The key insight of the definition is to treat these extensions as forms of downgrading and give them satisfactory technical treatment using the state-of-the-art information flow machinery.

cs.PL↗

arXiv2025

User Perceptions and Attitudes Toward Untraceability in Messaging Platforms

Mainstream messaging platforms offer a variety of features designed to enhance user privacy, such as password-protected chats and end-to-end encryption, which primarily protect message contents. Beyond contents, a lot can be inferred about people simply by tracing who sends and receives messages, when, and how often. This paper explores user perceptions of and attitudes toward "untraceability", defined as preventing third parties from tracing who communicates with whom, to inform the design of privacy-enhancing technologies and untraceable communication protocols. Through a vignette-based qualitative study with 189 participants, we identify a diverse set of features that users perceive to be useful for untraceable messaging, ranging from using aliases instead of real names to VPNs. Through a reflexive thematic analysis, we uncover three overarching attitudes that influence the support or rejection of untraceability in messaging platforms and that can serve as a set of new privacy personas: privacy fundamentalists, who advocate for privacy as a universal right; safety fundamentalists, who support surveillance for the sake of accountability; and optimists, who advocate for privacy in principle but also endorse exceptions in idealistic ways, such as encryption backdoors. We highlight a critical gap between the threat models assumed by users and those addressed by untraceable communication protocols. Many participants understood untraceability as a form of anonymity, but interpret it as senders and receivers hiding their identities from each other, rather than from external network observers. We discuss implications for design of strategic communication and user interfaces of untraceable messaging protocols, and propose framing untraceability as a form of "altruistic privacy", i.e., adopting privacy-enhancing technologies to protect others, as a promising strategy to foster broad adoption.

cs.CR↗

arXiv2024

Metadata Privacy Beyond Tunneling for Instant Messaging

Transport layer data leaks metadata unintentionally -- such as who communicates with whom. While tools for strong transport layer privacy exist, they have adoption obstacles, including performance overheads incompatible with mobile devices. We posit that by changing the objective of metadata privacy for $\textit{all traffic}$, we can open up a new design space for pragmatic approaches to transport layer privacy. As a first step in this direction, we propose using techniques from information flow control and present a principled approach to constructing formal models of systems with metadata privacy for $\textit{some}$, deniable, traffic. We prove that deniable traffic achieves metadata privacy against strong adversaries -- this constitutes the first bridging of information flow control and anonymous communication to our knowledge. Additionally, we show that existing state-of-the-art protocols can be extended to support metadata privacy, by designing a novel protocol for $\textit{deniable instant messaging}$ (DenIM), which is a variant of the Signal protocol. To show the efficacy of our approach, we implement and evaluate a proof-of-concept instant messaging system running DenIM on top of unmodified Signal. We empirically show that the DenIM on Signal can maintain low-latency for unmodified Signal traffic without breaking existing features, while at the same time supporting deniable Signal traffic.

cs.CR↗

arXiv2023

OblivIO: Securing reactive programs by oblivious execution with bounded traffic overheads

Traffic analysis attacks remain a significant problem for online security. Communication between nodes can be observed by network level attackers as it inherently takes place in the open. Despite online services increasingly using encrypted traffic, the shape of the traffic is not hidden. To prevent traffic analysis, the shape of a system's traffic must be independent of secrets. We investigate adapting the data-oblivious approach the reactive setting and present OblivIO, a secure language for writing reactive programs driven by network events. Our approach pads with dummy messages to hide which program sends are genuinely executed. We use an information-flow type system to provably enforce timing-sensitive noninterference. The type system is extended with potentials to bound the overhead in traffic introduced by our approach. We address challenges that arise from joining data-oblivious and reactive programming and demonstrate the feasibility of our resulting language by developing an interpreter that implements security critical operations as constant-time algorithms.

cs.CR↗

arXiv2022

With a Little Help from My Friends: Transport Deniability for Instant Messaging

Traffic analysis for instant messaging (IM) applications continues to pose an important privacy challenge. In particular, transport-level data can leak unintentional information about IM -- such as who communicates with whom. Existing tools for metadata privacy have adoption obstacles, including the risks of being scrutinized for having a particular app installed, and performance overheads incompatible with mobile devices. We posit that resilience to traffic analysis must be directly supported by major IM services themselves, and must be done in a low-cost manner without breaking existing features. As a first step in this direction, we propose a hybrid messaging model that combines regular and deniable messages. We present a novel protocol for deniable instant messaging, which we call DenIM. DenIM is built on the principle that deniable messages can be made indistinguishable from regular messages with a little help from a user's friends. Deniable messages' network traffic can then be explained by a plausible cover story. DenIM achieves overhead proportional to the messages sent, as opposed to scaling with time or number of users. To show the effectiveness of DenIM, we implement a trace simulator, and show that DenIM's deniability guarantees hold against strong adversaries such as internet service providers.

cs.CR↗

arXiv2021

Towards Language-Based Mitigation of Traffic Analysis Attacks

Traffic analysis attacks pose a major risk for online security. Distinctive patterns in communication act as fingerprints, enabling adversaries to de-anonymise communicating parties or to infer sensitive information. Despite the attacks being known for decades, practical solution are scarce. Network layer countermeasures have relied on black box padding schemes that require significant overheads in latency and bandwidth to mitigate the attacks, without fundamentally preventing them, and the problem has received little attention in the language-based information flow literature. Language-based methods provide a strong foundation for fundamentally addressing security issues, but previous work has overwhelmingly assumed that interactive programs communicate over secure channels, where messages are undetectable by unprivileged adversaries. This assumption is too strong for online communication where packets can be trivially observed by eavesdropping. In this paper we introduce SELENE, a small language for principled, provably secure communication over channels where packets are publicly observable, and we demonstrate how our program level defence can reduce the latency and bandwidth overheads induced compared with program-agnostic defence mechanisms. We believe that our results constitute a step towards practical, secure online communication.

cs.PL↗

arXiv2020

Reconciling progress-insensitive noninterference and declassification

Practitioners of secure information flow often face a design challenge: what is the right semantic treatment of leaks via termination? On the one hand, the potential harm of untrusted code calls for strong progress-sensitive security. On the other hand, when the code is trusted to not aggressively exploit termination channels, practical concerns, such as permissiveness of the enforcement, make a case for settling for weaker, progress-insensitive security. This binary situation, however, provides no suitable middle point for systems that mix trusted and untrusted code. This paper connects the two extremes by reframing progress-insensitivity as a particular form of declassification. Our novel semantic condition reconciles progress-insensitive security as a declassification bound on the so-called progress knowledge in an otherwise progress or timing sensitive setting. We show how the new condition can be soundly enforced using a mostly standard information-flow monitor. We believe that the connection established in this work will enable other applications of ideas from the literature on declassification to progress insensitivity.

cs.PL↗

arXiv2019

A Dependently Typed Library for Static Information-Flow Control in Idris

Safely integrating third-party code in applications while protecting the confidentiality of information is a long-standing problem. Pure functional programming languages, like Haskell, make it possible to enforce lightweight information-flow control through libraries like MAC by Russo. This work presents DepSec, a MAC inspired, dependently typed library for static information-flow control in Idris. We showcase how adding dependent types increases the expressiveness of state-of-the-art static information-flow control libraries and how DepSec matches a special-purpose dependent information-flow type system on a key example. Finally, we show novel and powerful means of specifying statically enforced declassification policies using dependent types.

cs.PL↗

arXiv2011

Attacker Control and Impact for Confidentiality and Integrity

Language-based information flow methods offer a principled way to enforce strong security properties, but enforcing noninterference is too inflexible for realistic applications. Security-typed languages have therefore introduced declassification mechanisms for relaxing confidentiality policies, and endorsement mechanisms for relaxing integrity policies. However, a continuing challenge has been to define what security is guaranteed when such mechanisms are used. This paper presents a new semantic framework for expressing security policies for declassification and endorsement in a language-based setting. The key insight is that security can be characterized in terms of the influence that declassification and endorsement allow to the attacker. The new framework introduces two notions of security to describe the influence of the attacker. Attacker control defines what the attacker is able to learn from observable effects of this code; attacker impact captures the attacker's influence on trusted locations. This approach yields novel security conditions for checked endorsements and robust integrity. The framework is flexible enough to recover and to improve on the previously introduced notions of robustness and qualified robustness. Further, the new security conditions can be soundly enforced by a security type system. The applicability and enforcement of the new policies is illustrated through various examples, including data sanitization and authentication.

cs.PL↗