CSP 2020

Schedule

• Lec-1: Introduction (slides)
• Lec-2: OS Structure (slides)
• Unikernels: Library Operating Systems for the Cloud
• Singularity: Rethinking the Software Stack
• Lec-3: Microkernel (slides)
• From L3 to seL4: What Have We Learnt in 20 Years of L4 Microkernels?
• Scheduling-Context Capabilities A Principled, Light-Weight OS Mechanism for Managing Time
• Lec-4: File System General (slides)
• F2FS: A New File System for Flash Storage
• BetrFS: A Right-Optimized Write-Optimized File System
• Lec-5: NVM and File System (slides)
• NOVA-Fortis: A Fault-Tolerant Non-Volatile Main Memory File System
• Strata: A Cross Media File System
• Lec-6: Virtualization (slides)
• Live migration of virtual machines
• Memory resource management in VMware ESX server
• Lec-7: Isolation (slides)
• Nested Kernel: An Operating System Architecture for Intra-Kernel Privilege Separation
• CloudVisor: Retrofitting Protection of Virtual Machines in Multi-tenant Cloud with Nested Virtualization
• Lec-8: JVM (slides)
• Yak: A High-Performance Big-Data-Friendly Garbage Collector
• Don't Get Caught in the Cold, Warm-up Your JVM: Understand and Eliminate JVM Warm-up Overhead in Data-Parallel Systems
• Lec-9: Transaction (slides)
• Extracting more concurrency from distributed transactions
• Speedy transactions in multicore in-memory databases
• Lec-10: Architecture support for system security (slides)
• No need to hide: Protecting safe regions on commodity hardware
• ERIM: Secure, Efficient In-process Isolation with Memory Protection Keys
• Lec-11: Hardware Enclave (slides)
• SCONE: Secure Linux Containers with Intel SGX
• Graphene-SGX: A practical library OS for unmodified applications on SGX
• Lec-12: Hardware Support for OS (slides)
• HDFI: Hardware-Assisted Data-flow Isolation
• M3: A Hardware/Operating-System Co-design to Tame Heterogenous Manycores
• Lec-13: Security: Attack and Defense (slides)
• Code-pointer integrity
• Missing the point(er): On the effectiveness of code pointer integrity
• Lec-14: Data Privacy (slides)
• CryptDB: Protecting Confidentiality with Encrypted Query Processing
• Opaque: An Oblivious and Encrypted Distributed Analytics Platform
• Lec-15: Formal Verification (slides)
• Push-Button Verification of File Systems via Crash Refinement
• Using Crash Hoare logic for certifying the FSCQ file system

Final Projects

1. 微内核
2. 事务并发控制
3. 数据隐私保护
4. 体系结构支撑的操作系统安全增强
5. 语言虚拟机
6. 形式化验证
7. 非易失性内存

选题二维码：

时间节点：

TA: 杨璧丞   Email: bichengyang@sjtu.edu.cn