François Hublet

Last Name

Hublet

First Name

François

ORCID

0000-0001-5419-3125

Organisational unit

03634 - Basin, David / Basin, David

Show all metadata

Search Results

Publications 1 - 9 of 9

Mechanizing Privacy by Design
Basin, David; Hublet, François; Krstić, Srđan; et al. (2025)
CCS '25: Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security
Privacy by design requires integrating data protection into systems from the outset, during their design, rather than building it in later. Related legislation does not specify how to achieve this and mainstream languages and frameworks lack support for privacy by design. To address this long-standing problem, we have developed diferent, effective technical solutions. First, we have developed powerful logic-based tools that enforce formal data protection policies at runtime by controlling relevant system actions. Second, we have proposed methods and tools for integrating privacy models into system design models, enabling model-driven privacy enforcement. We report on our methods, tools, and practical experiences using them
User-Controlled Privacy: Taint, Track, and Control
Hublet, François; Basin, David; Krstić, Srđan (2024)
Proceedings on Privacy Enhancing Technologies
We develop the first language-based, Privacy by Design approach that provides support for a rich class of privacy policies. The policies are user-defined, rather than programmer-defined, and support fine-grained information flow restrictions (considering individual application inputs and outputs) with temporal constraints. Our approach, called Taint, Track, and Control (TTC), combines dynamic information-flow control and runtime verification to enforce these policies in the presence of malicious users and developers. We provide TTC's semantics and proofs of its correct enforcement, formalized in the Isabelle/HOL proof assistant. We also implement our approach in a web development framework and port three baseline applications from previous work into this framework for evaluation. Overall, our approach enforces expressive user-defined privacy policies with practical runtime performance.
Proactive Real-Time First-Order Enforcement
Hublet, François; Lima, Leonardo; Basin, David; et al. (2024)
Lecture Notes in Computer Science ~ Computer Aided Verification
Modern software systems must comply with increasingly complex regulations in domains ranging from industrial automation to data protection. Runtime enforcement addresses this challenge by empowering systems to not only observe, but also actively control, the behavior of target systems by modifying their actions to ensure policy compliance. We propose a novel approach to the proactive real-time enforcement of policies expressed in metric first-order temporal logic (MFOTL). We introduce a new system model, define an expressive MFOTL fragment that is enforceable in that model, and develop a sound enforcement algorithm for this fragment. We implement this algorithm in a tool called WhyEnf and carry out a case study on enforcing GDPR-related policies. Our tool can enforce all policies from the study in real-time with modest overhead. Our work thus provides the first tool-supported approach that can proactively enforce expressive first-order policies in real time.
Real-Time Policy Enforcement with Metric First-Order Temporal Logic
Hublet, François; Basin, David; Krstić, Srđan (2022)
Lecture Notes in Computer Science ~ Computer Security – ESORICS 2022
Correctness and regulatory compliance of today’s software systems are crucial for our safety and security. This can be achieved with policy enforcement: the process of monitoring and possibly modifying system behavior to satisfy a given policy. The enforcer’s capabilities determine which policies are enforceable. We study the enforceability of policies specified in metric first-order temporal logic (MFOTL) with enforcers that can cause and suppress different system actions in real time. We consider an expressive safety fragment of MFOTL and show that a policy from that fragment is enforceable if and only if it is equivalent to a policy in a simpler, syntactically defined MFOTL fragment. We then propose an enforcement algorithm for all monitorable policies from the latter fragment, and show that our EnfPoly enforcer outperforms state-of-the-art tools.
Where the Borders Lie: Mapping Cross-Border Communities in 10 Western European Countries
Sallard, Aurore; Hublet, François (2025)
Transportation Research Record
With the deepening of European integration, Western Europe has witnessed the emergence of highly interconnected cross-border living areas. So far, these areas have received rather limited attention from both quantitative research and public policy. The COVID-19 pandemic dramatically exposed the limitations of the status quo: with travel restrictions imposed at administrative borders and limited cross-border crisis management, the daily life of people in border regions was affected in a disproportionate way. In an effort to better understand the geography of cross-border communities, this paper presents the first large-scale quantitative analysis of cross-border communities in Western Europe. We apply the Louvain community detection algorithm to a transnational, fine-grained dataset gathering commuter flows across 10 Western European countries. This allows us to produce the first comprehensive transnational mapping of communities in these countries and identify five main cross-border living areas. Based on these findings, we put forward policy recommendations aimed at improving the design of mobility censuses and developing new institutional frameworks in cross-border regions.
Scaling Up Proactive Enforcement
Hublet, François; Lima, Leonardo; Basin, David; et al. (2025)
Lecture Notes in Computer Science ~ Computer Aided Verification. 37th International Conference, CAV 2025 Zagreb, Croatia, July 23–25, 2025 Proceedings, Part III
Runtime enforcers receive events from a system and output commands ensuring the system’s policy compliance. Proactive enforcers extend traditional (reactive) enforcers by emitting commands at any time, rather only as a response to system actions. However, proactive enforcers have so far lacked support for many useful policy features. This, along with the existing tools’ poor performance, hinders their adoption. We present a performance-optimized, proactive enforcement algorithm for a rich policy language: metric first-order temporal logic with function applications, aggregations, and bindings. We have implemented this algorithm in EnfGuard, the first proactive enforcer tool that supports the above constructs. We evaluated our tool using a novel set of six benchmarks containing both real-world and synthetic policies and logs, demonstrating that it enforces realistic policies out-of-the-box and achieves the necessary performance to be used in real-time systems.
Instrumenting Runtime Enforcement
Hublet, François; Basin, David; Hu, Linda; et al. (2025)
Lecture Notes in Computer Science ~ Runtime Verification
Runtime enforcement ensures that a running system complies with a property by observing and modifying the system’s actions. In practice, the property is often defined in terms of high-level, abstract events, while the system’s behavior consists of low-level, concrete actions. The relationship between actions and events is established in the instrumentation process, where developers must ensure that (i) system actions report the right events, and (ii) the necessary modifications to the system’s behavior are correctly enforced. However, the abstraction gap between a high-level property and low-level actions makes this process error-prone. In this paper, we refine an existing formal model of runtime enforcement, which leaves instrumentation implicit, into a more precise model that explicitly accounts for instrumentation. We propose a correctness criterion for instrumentation and present a novel library, called InstrLib, that instruments Python applications for runtime enforcement.
IDL-PMCFG, a Grammar Formalism for Describing Free Word Order Languages
Hublet, François (2022)
Journal of Logic, Language and Information
We introduce Interleave-Disjunction-Lock parallel multiple context-free grammars (IDL-PMCFG), a novel grammar formalism designed to describe the syntax of free word order languages that allow for extensive interleaving of grammatical constituents. Though interleaved constituents, and especially the so-called hyperbaton, are common in several ancient (Classical Latin and Greek, Sanskrit...) and modern (Hungarian, Finnish...) languages, these syntactic structures are often difficult to express in existing formalisms. The IDL-PMCFG formalism combines Seki et al.'s parallel multiple context-free grammars (PMCFG) with Nederhof and Satta's IDL expressions. We define the semantics of IDL-PMCFGs and study their expressivity, proving that IDL-PMCFG extends both PMCFG and IDL-CFG (context-free grammars equipped with IDL expressions) and that IDL-PMCFG parsing is NP-hard. We then introduce COMP (A) over bar, a programming language extending Ranta's Grammatical Framework (GF) and built as a high-level front-end formalism to IDL-PMCFG for practical grammar development. We present a parsing algorithm for IDL-PMCFG inspired by earlier Earley-style PMCFG parsing algorithms and Nederhof and Satta's IDL graphs and give a worst-case estimate of its complexity as a function of several metrics on IDL expressions, the size of the input and a new notion of the G-density of a language.
Enforcing the GDPR
Hublet, François; Basin, David; Krstić, Srđan (2024)
Lecture Notes in Computer Science ~ Computer Security – ESORICS 2023
Violations of data protection laws such as the General Data Protection Regulation (GDPR) are ubiquitous. Currently building IT support to implement such laws is difficult and the alternatives such as manual controls augmented by auditing are limited and scale poorly. This calls for new automated enforcement techniques that can build on, and enforce, a formalization of the law. In this paper, we present the first enforceable specification of a core set of GDPR provisions, centered on data-subject rights, and describe an architecture that automatically enforces this specification in web applications. We evaluate our architecture by implementing three case studies and show that our approach incurs only modest development and runtime overhead, while covering the most relevant privacy-related aspects of GDPR that can be enforced at runtime.

Publications 1 - 9 of 9

François Hublet

Last Name

First Name

ORCID

Organisational unit

Filters

Search Results