Static Information Flow Control Made Simpler

2025-05-03 0 0 870.6KB 12 页 10玖币

侵权投诉

HEMANT GOUNI, University of Minnesota, USA

JONATHAN ALDRICH, Carnegie Mellon University, USA

Static information ow control (IFC) systems provide the ability to restrict data ows within a program,

enabling vulnerable functionality or condential data to be statically isolated from unsecured data or program

logic. Despite the wide applicability of IFC as a mechanism for guaranteeing condentiality and integrity—

the fundamental properties on which computer security relies— existing IFC systems have seen little use,

requiring users to reason about complicated mechanisms such as lattices of security labels and dual notions

of condentiality and integrity within these lattices. We propose a system that diverges signicantly from

previous work on information ow control, opting to reason directly about the data that programmers already

work with. In doing so, we naturally and seamlessly combine the clasically separate notions of condentiality

and integrity into one unied framework, further simplifying reasoning. We motivate and showcase our work

through two case studies on TLS private key management: one for Rocket, a popular Rust web framework,

and another for Conduit, a server implementation for the Matrix messaging service written in Rust.

CCS Concepts:

•Software and its engineering →Formal software verication

;

Specication lan-

guages.

Additional Key Words and Phrases: Information Flow Control, Security Type Systems, Accessible Correctness

1 INTRODUCTION

Security is a paramount concern in a pervasively digital world. The vast increase in digitization of

the past decade has come with a proportional increase in the severity of data breaches [Warren

et al

2016], warranting renewed research into accessible, yet powerful, methods of declaring and

enforcing security specications. Information ow control is a program analysis technique that

aims to prevent undesirable data ows. For example, in a program implementing a simple web

application for performing authentication, there may be modules for (1) performing network I/O,

(2) validating user input, (3) checking passwords, and (4) interacting with a database. A reasonable

information ow specication, shown in Fig. 1, might be that (1) should never ow to (3) or (4),

and that data from (4) should never ow to (1). Green (solid) arrows in the diagram denote the

ows required for the program to function, and red (dashed) arrows denote the ows which must

be prevented to ensure the program’s security. A ow from, for instance, (1) to (4), occurs when

data from (1), or which is transitively dependent on (1), ows to (4). Note that certain ows in the

diagram, such as from (1) to (4), are denied directly but permitted transitively— specically, after

data from (1) passes through (2). This is addressed during the case study in Section 2.

Fig. 1. Permied flows in our example program

Authors’ addresses: Hemant Gouni, gouni008@umn.edu, University of Minnesota, Minneapolis, Minnesota, USA; Jonathan

Aldrich, jonathan.aldrich@cs.cmu.edu, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA.

arXiv:2210.12996v1 [cs.PL] 24 Oct 2022

2 Hemant Gouni and Jonathan Aldrich

A classical information ow control system [Myers 1999; Simonet 2003] might support the

specication of the ow architecture in Fig. 1 by providing two lattices: one for reasoning about

condentiality, or the property that condential data does not leak to inappropriately visible places,

and one for integrity, or the property that untrusted data does not propagate to inappropriately

integral places. All data in the program must have a label relevant to each lattice, denoting its

levels of condentiality and integrity. Two separate lattices are required for each property owing

to the duality between them: two distinct and opposing invariants must be enforced when data

is labeled as both highly condential and highly integral, such as with

db_handle

in Fig. 1. First,

it must never ow to data labeled as being of low condentiality, such as

network_io

. Second,

data labeled as being of low integrity, again like

network_io

, must never ow to

db_handle

. This

separate treatment complicates reasoning— for example, Jif [Pullicino 2014], a state of the art IFC

system for Java, provides entirely new (dual) semantics for lattice operations when reasoning about

integrity versus condentiality.

Our system resolves this issue by presenting a single, straightforward abstraction for declaring

information ow policies, simplifying specications while retaining expressivity. Instead of organiz-

ing data inside a lattice and reasoning about ows in the context of it, we opt to allow programmers

to directly specify which ows between places in a program are not permitted, as presented in the

architecture in Fig. 1. A declaration

flow b ->! c

states that data aected by variable

cannot

ow to variable

, and a declaration

flow mod network_io ->! mod db_handle

states that data

aected by the

network_io

module cannot ow to the

db_handle

module. We will refer to the part

before the arrow as the source, and the part after as the destination. This streamlined annotation

language contributes to a system which is:

(1) Uniform:

a ow annotation

flow b ->! c

may be an integrity specication, a condentiality

specication, or potentially both— the programmer need not shift their reasoning

(2) Incremental:

our approach to ow annotations encourages partial and local specications

on the way to proving higher level program properties, and

(3) Simple:

we provide a small number of straightforward constructs which are highly general

and composable, minimizing changes needed to the semantics of the language and easing

adoption of the system by new users.

We will explore these properties further by analyzing cryptographic key management in two

popular Rust programs, Rocket and Conduit. A brief formal description of our IFC system, as an

extension to the Rust type system, is provided in the appendix for the curious reader.

2 MOTIVATION: MANAGING KEYS

2.1 Case Study: Rocket

Rocket is a fully edged and widely used HTTP framework for Rust. Like many web frameworks, it

provides optional support for serving trac over Transport Layer Security, or TLS, connections. TLS

is an essential feature for securing data between clients, such as browsers, and servers, encrypting

data in transit. A critical component of TLS is a public-private keypair held by the server, in this

case Rocket. Each domain which aims to communicate securely with web browsers and clients at

large must obtain a certied keypair, which is valid for any trac served by it. While a typical web

service consists of a large number of physical servers, each of them may use the same TLS keypair,

assuming they are serving a single domain. This is convenient, but risky— leakage of the private

key for a domain from any of its servers risks compromising the security of the entire service. It is

essential, then, that this does not occur, and an IFC system may be able to provide that assurance.

Most of our discussion will be directed at the particular Rocket code path that deals with con-

ditionally conguring TLS functionality, shown in Fig. 2. Specically, we analyze the function

Static Information Flow Control Made Simpler 3

1flow self.config.tls.key ->!fn io!();

2flow self.config.tls.key ->! *;

4...

6let mut listener: Either<TcpListener, TlsListener> =

7Left(TcpListener::bind(addr).await.map_err(ErrorKind::Bind)?);

9if self.config.tls_enabled() {

10 if let Some(ref config) =self.config.tls

11 with flow self.config.tls.key -> config {

13 let conf =config.to_native_config().map_err(ErrorKind::Io)?

14 with flow self.config.tls.key -> conf;

16 flow self.config.tls.key -> listener;

18 listener =

19 Right(TlsListener::bind(addr, conf).await.map_err(ErrorKind::Bind)?);

20 }

21 }

23 listener =allow listener;

25 ...

Fig. 2. Verifying non-leakage of TLS key data in Rocket

default_tcp_http_server

in le

core/lib/src/server.rs

, on commit

2fc4b156

of the Rocket

git repository. In order to render this section of code amenable to information ow verication, some

minimal refactoring was required; we will return to this later. We focus our attention here because it

is the primary part of the codebase where key data is accessed directly (through

to_native_config

and

TlsListener::bind

on lines 13 and 19), increasing the potential for leaks and need for veri-

cation. Verication of the latter two functions is not as interesting, because their implementation

is largely straightforward or reliant on primitives provided by Rustls, a TLS library for Rust. A

summary of the displayed Rocket code follows.

Ignoring the information ow constructs, the code in Fig. 2:

•On lines 6 and 7: Binds a variable, listener, which initially holds a TCP socket

•On lines 9 and 10: Checks that TLS is enabled and that a TLS conguration is provided

•

In lines 13 through 19: Extracts the provided TLS conguration into a structure understood

by TlsListener::bind and calls it, setting listener to the returned TLS socket.

We now discuss the IFC specications for

self.config.tls.key

, which contains key data, in

Fig. 2. The ow declaration on the rst line prohibits the private key from owing transitively to

any functions which could perform I/O operations, such as those in

std::io

std::fs

std::net

std::ffi

, and

std::os

. The same property could be expressed as a series of individual ow

declarations on each relevant namespace, but the use of a macro here provides a convenient

abstraction. The next declaration employs a special place understood by ow rules:

, which applies

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

StaticInformationFlowControlMadeSimplerHEMANTGOUNI,UniversityofMinnesota,USAJONATHANALDRICH,CarnegieMellonUniversity,USAStaticinformationflowcontrol(IFC)systemsprovidetheabilitytorestrictdataflowswithinaprogram,enablingvulnerablefunctionalityorconfidentialdatatobestaticallyisolatedfromunsecureddatao...

展开>> 收起<<

Static Information Flow Control Made Simpler.pdf

共12页,预览3页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Static Information Flow Control Made Simpler

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: