Identifying {Cache-Based} Side Channels through {Secret-Augmented} Abstract Interpretation S Wang, Y Bao, X Liu, P Wang, D Zhang, D Wu 28th USENIX security symposium (USENIX security 19), 657-674, 2019 | 51 | 2019 |
Reachability types: tracking aliasing and separation in higher-order functional programs Y Bao, G Wei, O Bračevac, Y Jiang, Q He, T Rompf Proceedings of the ACM on Programming Languages 5 (OOPSLA), 1-32, 2021 | 15 | 2021 |
Verifying verified code S Priya, X Zhou, Y Su, Y Vizel, Y Bao, A Gurfinkel Innovations in Systems and Software Engineering 18 (3), 335-346, 2022 | 10 | 2022 |
Conditional effects in fine-grained region logic Y Bao, GT Leavens, G Ernst Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs …, 2015 | 10 | 2015 |
Unifying separation logic and region logic to allow interoperability Y Bao, GT Leavens, G Ernst Formal Aspects of Computing 30, 381-441, 2018 | 8 | 2018 |
Sok: Demystifying binary lifters through the lens of downstream applications Z Liu, Y Yuan, S Wang, Y Bao 2022 IEEE Symposium on Security and Privacy (SP), 1100-1119, 2022 | 7 | 2022 |
Graph irs for impure higher-order languages: Making aggressive optimizations affordable with precise effect dependencies O Bračevac, G Wei, S Jia, S Abeysinghe, Y Jiang, Y Bao, T Rompf Proceedings of the ACM on Programming Languages 7 (OOPSLA2), 400-430, 2023 | 5 | 2023 |
Polymorphic reachability types: Tracking freshness, aliasing, and separation in higher-order generic programs G Wei, O Bračevac, S Jia, Y Bao, T Rompf arXiv preprint arXiv:2307.13844, 2023 | 4 | 2023 |
HACCLE: metaprogramming for secure multi-party computation Y Bao, K Sundararajah, R Malik, Q Ye, C Wagner, N Jaber, F Wang, ... Proceedings of the 20th ACM SIGPLAN International Conference on Generative …, 2021 | 4 | 2021 |
Reasoning about frame properties in object-oriented programs Y Bao | 4 | 2017 |
Cache Refinement Type for Side-Channel Detection of Cryptographic Software K Jiang, Y Bao, S Wang, Z Liu, T Zhang Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications …, 2022 | 3 | 2022 |
Bounded model checking for llvm S Priya, X Zhou, Y Su, Y Vizel, Y Bao, A Gurfinkel CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN–FMCAD 2022, 214, 2022 | 3 | 2022 |
A methodology for invariants, framing, and subtyping in JML Y Bao, GT Leavens Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter …, 2018 | 3 | 2018 |
Translating separation logic into dynamic frames using fine-grained region logic Y Bao, GT Leavens, G Ernst Technical Report CS-TR-13-02a, Computer Science, University of Central …, 2014 | 3 | 2014 |
Graph IRs for Impure Higher-Order Languages (Technical Report) O Bračevac, G Wei, S Jia, S Abeysinghe, Y Jiang, Y Bao, T Rompf arXiv preprint arXiv:2309.08118, 2023 | 1 | 2023 |
HACCLE: An Ecosystem for Building Secure Multi-Party Computations Y Bao, K Sundararajah, R Malik, Q Ye, C Wagner, F Wang, MH Ameri, ... CoRR, 2020 | 1 | 2020 |
Modeling Reachability Types with Logical Relations Y Bao, G Wei, O Bračevac, T Rompf arXiv preprint arXiv:2309.05885, 2023 | | 2023 |
HACCLE: Metaprogramming for Secure Multi-Party Computation--Extended Version Y Bao, K Sundararajah, R Malik, Q Ye, C Wagner, N Jaber, F Wang, ... arXiv preprint arXiv:2009.01489, 2020 | | 2020 |
Fine-Grained Region Logic Y Bao, GT Leavens, G Ernst | | 2016 |
Fine Grained Region Logic for Reasoning about Frame Properties Y Bao, GT Leavens | | 2013 |