23 HiStar/FSCQ

1 . Today’s Papers EECS 262a • Making Information Flow Explicit in HiStar, Nickolai Zeldovich, Silas Boyd-Wickizer, Eddie Kohler, and David Mazières. Appears in Advanced Topics in Computer Systems Proceedings of the 7th USENIX Symposium on Operating Systems Lecture 23 Design and Implementation (OSDI), 2006\ • Using Crash Hoare Logic for Certifying the FSCQ File System, Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. Appears in Symposium on HiStar/FSCQ Operating Systems Principles (SOSP), 2015 November 15th, 2018 John Kubiatowicz • Thoughts? (With slides from Ion Stoica and Ali Ghodsi) Electrical Engineering and Computer Sciences University of California, Berkeley http://www.eecs.berkeley.edu/~kubitron/cs262 11/15/2018 cs262a-F18 Lecture-23 2 Motivation Main idea • Security vulnerabilities discovered in all kinds of apps • Small kernel (20k LoC) that controls information flow • Buffer overflows, format string issues, SQL injection, JS injection, • Don’t care about bugs in programs, make sure kernel isn’t buggy temp file races, integer overflows • Control the information flow between potentially buggy programs • Security implemented at many different levels • Seen this idea before? • Web app implements its own logic, e.g. private Facebook posts • Web servers implement access to different directories (.htaccess) • Example • OS implements its own ACLs, users, SU, … • Antivirus needs to scan all your files. • Hardware implements security, page tables, etc • It will see confidential information. • If the AV code is malicious, it can communicate that code out over the • Bugs could exist anywhere, high level info can be leaked Internet at any level! • Kernel can simply now allow AV to send info anywhere • Meltdown leaking secret webapp info to another tenant 11/15/2018 cs262a-F18 Lecture-23 3 11/15/2018 cs262a-F18 Lecture-23 4 

2 . Military research in the 70s: Bell LaPadula Military research in the 70s: Biba • Bell Lapadula • Biba • Preserve confidentiality • Preserve integrity / trustworthiness • Subjects reading/writing Objects • Who would you trust when receiving information? • Subjects and Objects given a level, e.g. 1…4 (unclassified…top secret) • No write up • Subject at level i cannot write object at level j when i < j • No read up • Cannot authoritatively provide information to the upper • Subject at level i cannot read object at level j when i < j levels • e.g. anonymous user reading root’s files (could leak /etc/passwd) • No read down • Subject at level i cannot read object at level j when i > j • No write down • Cannot trust information from lower levels • Subject at level i cannot write object at level j when i > j • e.g. root writing to /user/anonymous (could leak secret info to anonymous) 11/15/2018 cs262a-F18 Lecture-23 5 11/15/2018 cs262a-F18 Lecture-23 6 Military Operating Systems Information Flow Control (IFC) • Early OS:s implemented these ideas for file systems • How should we track information flow? • Policies on how top secret or classified information could be • Associate a Label with the data handled • Label follows data when it moves around • Reading and writing of files were protected • Labels determine what you can do with the data • How is it different from today’s file systems and their security? • e.g. SSN cannot be sent to any other computer • Application level concepts wouldn’t get these benefits • OS doesn’t know about the app data • HiStar exposes these security mechanisms to all apps • Information Flow as basic OS mechanisms exposed to apps! • Can implement Bell Lapadula and Biba in any app! 11/15/2018 cs262a-F18 Lecture-23 7 11/15/2018 cs262a-F18 Lecture-23 8 

3 . Example: Virus Scanner Problems Today • AV Scanner/Helper • Any process can be hacked! • Read virus DB (signatures) • Read all files • AV Scanner sending private • Read/write tmp files data to internet • Write to screen scan status • Prevent scanner from any communication with network • Update daemon • AV Scanner Colluding with • Read/write data to Internet to fetch latest virus DB Update Daemon • Write to the virus DB to update it • But update daemon needs to communicate with network • Must prevent unauthorized IPC between processes • Can we protect files from corruption and leakage to • AV Scanner write data to /tmp subsequently retrieved by outside? the update daemon • Must prevent unauthorized communication through file system 11/15/2018 cs262a-F18 Lecture-23 9 11/15/2018 cs262a-F18 Lecture-23 10 Problems today Information Flow to save us! • OS today have protection • File systems with RBAC • Process protection • Memory protection • What’s the problem? • They ignore information flow • Process P can read a secret file it has access to and write it to a public file • Information Flow Control (IFC): • Process P does so either maliciously or by getting hacked, e.g. buffer – Files & processes colored overflow – Label private stuff RED • OSs allow violating Bell Lapadula (“no write – Label public stuff GREEN down”violated) • Enforce the arrows in the chart 11/15/2018 cs262a-F18 Lecture-23 11 11/15/2018 cs262a-F18 Lecture-23 12 

4 . Kernels Objects Information Flow: Labels & Categories • Six kernel objects • Every Kernel Object has a label • Segment (data itself), array of bytes • Label tells you the security property of the information • Thread inside an object • Address space • Since an object (e.g. Thread) might contain multiple types of information, labels contain multiple Categories (think of • Device (network) a category as a color) • Gate (IPC)* • HiStar will only allow kernel objects to interact (information • Container (“directory”), ever kernel object inside a to flow) if two kernel objects have “consistent” labels, i.e. container implement Bell Lapadula/Biba • All of Unix implemented on top of the 6 objects! Segment Segment Thread (Data Array) (Data Array) 11/15/2018 cs262a-F18 Lecture-23 13 11/15/2018 cs262a-F18 Lecture-23 14 Antivirus example fixed with IFC: AV explained in full ? • Colors (categories) have levels, own, 0 lowest, 1 default, 3 highest • Bob marks all User Data as color {bw0,br3,1}, i.e. color bobwrite=0, bobread=3, all other colors = 1 • wrap creates and owns v (virus) category, and owns read category (can downgrade and bypass v and r restrictions) • Great. But how do we get the AV result to the terminal screen? • wrap spawns virus scanner and helper with v level 3, /tmp with v level 3 • Process creating a category (color) owns it: it can declassify it and bypass restrictions on that category. • AV/helper cannot communicate with network, update daemon, because they don’t have color v=3, it can write secrets to /tmp (but • Small 140 line wrapper script extracts the AV output and prints it others cannot read it) • AV/helper cannot corrupt files, because they don’t have bw permission • All communication through trusted 140 line wrap 11/15/2018 cs262a-F18 Lecture-23 15 11/15/2018 cs262a-F18 Lecture-23 16 

5 . Unix vs IFC Conclusion • Current OSs have too many aspects that need to be secured • Sloppy code in many places lead to vulnerabilities • How is this different from Unix? • HiStar offers a minimalistic kernel that exposes We just have to be careful with permissions, right? information flow • No, HiStar tracks information flow! • Six objects in the kernel • Each object has a label (categories/colors) • Any information flow out of AV gets tainted as special • Information flow controlled between objects virus permission v3 • All of Unix implemented on top of these few abstractions • If you don’t have v3, AV scanner cannot leak to you. No • New applications can implement security using these matter how buggy AV/Helper is, no matter how many abstractions buffer overflows or malicious code snippets it has! • In Unix, AV scanner might by mistake leak information to a public file, screen, or network 11/15/2018 cs262a-F18 Lecture-23 17 11/15/2018 cs262a-F18 Lecture-23 18 Zooming out Is this a good paper? • Radically different approach to OSs. • What were the authors’ goals? • DiscretionaryAccessControl vs MandatoryAccessControl • What about the evaluation/metrics? • Dynamic assignment of labels? • Did they convince you that this was a good • Let data go wherever, but labels follow: Asbestos OS system/approach? • Gives ability to leak information • Were there any red-flags? • Attacks the problem with a small microkernel • Everything else implemented on top of it • What mistakes did they make? • All future applications benefit from the security of HiStar • Does the system/approach meet the “Test of Time” challenge? • Great bold paper! Realistic implementation. • How would you review this paper today? • Why didn’t it have more impact? 11/15/2018 cs262a-F18 Lecture-23 19 11/15/2018 cs262a-F18 Lecture-23 20 

6 . How to build correct filesystems? • Stare at the code really hard – Have lots of design reviews – Humans miss design flaws all the time • Alternative: Build automatically checkable implementation BREAK – Needs to be able to specify checkable invariants – Automatic generation of code from proof • What is hard about this? – Lots of things – Complex features hard to specify invariants – Non-atomic operations combine together into atomic state transitions – CRASH behavior: what happens when a crash occurs? • FSCQ filesystem: Tackle correctness in the face of crashes – Subset of POSIX 11/15/2018 cs262a-F18 Lecture-23 22 FSCQ in a nutshell Example specifications • Pre-and-Post conditions + possibilities after crash • Address spaces to build atomic actions 11/15/2018 cs262a-F18 Lecture-23 23 11/15/2018 cs262a-F18 Lecture-23 24 

7 . POSIX specification: all or nothing Write-ahead logging: FSCQLog • Prove abstraction/functionality of a write-ahead log, then use that functionality for FSCQ • Many of the POSIX calls are not specific about semantics under failure. – FSCQ takes an all-or-nothing stand for ambiguous cases 11/15/2018 cs262a-F18 Lecture-23 25 11/15/2018 cs262a-F18 Lecture-23 26 Performance of FSCQ Is this a good paper? • What were the authors’ goals? • What about the evaluation/metrics? • Did they convince you that this was a good system/approach? • Were there any red-flags? • What mistakes did they make? • Does the system/approach meet the “Test of Time” challenge? • How would you review this paper today? 11/15/2018 cs262a-F18 Lecture-23 27 11/15/2018 cs262a-F18 Lecture-23 28