Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types

被引:0
作者
Boruch-Gruszecki, Aleksander [1 ]
Ghosn, Adrien [2 ]
Payer, Mathias [3 ]
Pit-Claudel, Clement [3 ]
机构
[1] Charles Univ Prague, Prague, Czech Republic
[2] Microsoft, Azure Res, Reading, England
[3] Ecole Polytech Fed Lausanne, Lausanne, Switzerland
来源
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL | 2024年 / 8卷 / OOPSLA期
关键词
type systems; security; object capabilities; compartmentalization; PROTECTION;
D O I
10.1145/3689751
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Modern software needs fine-grained compartmentalization, i.e., intra-process isolation. A particularly important reason for it are supply-chain attacks, the need for which is aggravated by modern applications depending on hundreds or even thousands of libraries. Object capabilities are a particularly salient approach to compartmentalization, but they require the entire program to assume a lack of ambient authority. Most of existing code was written under no such assumption; effectively, existing applications need to undergo a rewrite-the-world migration to reap the advantages of ocap. We propose gradual compartmentalization, an approach which allows gradually migrating an application to object capabilities, component by component in arbitrary order, all the while continuously enjoying security guarantees. The approach relies on runtime authority enforcement and tracking the authority of objects the type system. We present Gradient, a proof-of- concept gradual compartmentalization extension to Scala which uses Enclosures and Capture Tracking as its key components. We evaluate our proposal by migrating the standard XML library of Scala to Gradient.
引用
收藏
页数:27
相关论文
共 68 条
[1]  
Amin Nada, 2016, A List of Successes that can Change the World. Essays Dedicated to Philip Wadler on the Occasion of his 60th Birthday. LNCS 9600, P249, DOI 10.1007/978-3-319-30936-1_14
[2]  
Amin N, 2014, ACM SIGPLAN NOTICES, V49, P233, DOI [10.1145/2714064.2660216, 10.1145/2660193.2660216]
[3]  
[Anonymous], 2006, Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control
[4]   Foundational proof-carrying code [J].
Appel, AW .
16TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2001, :247-256
[5]   RUDRA: Finding Memory Safety Bugs in Rust at the Ecosystem Scale [J].
Bae, Yechan ;
Kim, Youngsuk ;
Askar, Ammar ;
Lim, Jungwon ;
Kim, Taesoo .
PROCEEDINGS OF THE 28TH ACM SYMPOSIUM ON OPERATING SYSTEMS PRINCIPLES, SOSP 2021, 2021, :84-99
[6]  
Bittau Andrea, 2008, P 5 USENIX S NETWORK
[7]  
Boruch-Gruszecki Aleksander, 2024, Zenodo, DOI 10.5281/ZENODO.13385386
[8]   Capturing Types [J].
Boruch-Gruszecki, Aleksander ;
Odersky, Martin ;
Lee, Edward ;
Lhotak, Ondrej ;
Brachthaeuser, Jonathan .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2023, 45 (04)
[9]   A case for DOT: Theoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning [J].
Boruch-Gruszecki, Aleksander ;
Wasko, Radoslaw ;
Xu, Yichen ;
Parreaux, Lionel .
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2022, 6 (OOPSLA)
[10]  
Boruch-Gruszecki Aleksander, 2024, Gradient: migrated scala-xml, DOI [10.5281/zenodo.13385375, DOI 10.5281/ZENODO.13385375]