diff --git a/data/desc.txt b/data/desc.txt index 1d932ba..9dfac69 100644 --- a/data/desc.txt +++ b/data/desc.txt @@ -1,3 +1,3 @@ -Fat Pointers for Temporal Memory Safety of C -Zhou, Jie, et al. “Fat Pointers for Temporal Memory Safety of C.” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA1, Apr. 2023, pp. 316–47. Crossref, https://doi.org/10.1145/3586038. -Temporal memory safety bugs, especially use-after-free and double free bugs, pose a major security threat to C programs. Real-world exploits utilizing these bugs enable attackers to read and write arbitrary memory locations, causing disastrous violations of confidentiality, integrity, and availability. Many previous solutions retrofit temporal memory safety to C, but they all either incur high performance overhead and/or miss detecting certain types of temporal memory safety bugs. In this paper, we propose a temporal memory safety solution that is both efficient and comprehensive. Specifically, we extend Checked C, a spatially-safe extension to C, with temporally-safe pointers. These are implemented by combining two techniques: fat pointers and dynamic key-lock checks. We show that the fat-pointer solution significantly improves running time and memory overhead compared to the disjoint-metadata approach that provides the same level of protection. With empirical program data and hands-on experience porting real-world applications, we also show that our solution is practical in terms of backward compatibility---one of the major complaints about fat pointers. \ No newline at end of file +A Pretty Expressive Printer +Porncharoenwase, Sorawee, et al. “A Pretty Expressive Printer.” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2, Oct. 2023, pp. 1122–49. Crossref, https://doi.org/10.1145/3622837. +Pretty printers make trade-offs between the expressiveness of their pretty printing language, the optimality objective that they minimize when choosing between different ways to lay out a document, and the performance of their algorithm. This paper presents a new pretty printer, Π e , that is strictly more expressive than all pretty printers in the literature and provably minimizes an optimality objective. Furthermore, the time complexity of Π e is better than many existing pretty printers. When choosing among different ways to lay out a document, Π e consults a user-supplied cost factory , which determines the optimality objective, giving Π e a unique degree of flexibility. We use the Lean theorem prover to verify the correctness (validity and optimality) of Π e , and implement Π e concretely as a pretty printer that we call PrettyExpressive. To evaluate our pretty printer against others, we develop a formal framework for reasoning about the expressiveness of pretty printing languages, and survey pretty printers in the literature, comparing their expressiveness, optimality, worst-case time complexity, and practical running time. Our evaluation shows that PrettyExpressive is efficient and effective at producing optimal layouts. PrettyExpressive has also seen real-world adoption: it serves as a foundation of a code formatter for Racket. \ No newline at end of file diff --git a/data/history.txt b/data/history.txt index 4684971..bdfd3db 100644 --- a/data/history.txt +++ b/data/history.txt @@ -32,4 +32,5 @@ https://doi.org/10.1145/3656456 https://doi.org/10.1145/3622828 https://doi.org/10.1145/3632882 https://doi.org/10.1145/3607862 -https://doi.org/10.1145/3586038 \ No newline at end of file +https://doi.org/10.1145/3586038 +https://doi.org/10.1145/3622837 \ No newline at end of file diff --git a/data/next.txt b/data/next.txt index 0bf5ba9..7e8e3bd 100644 --- a/data/next.txt +++ b/data/next.txt @@ -1 +1 @@ -https://doi.org/10.1145/3586038 \ No newline at end of file +https://doi.org/10.1145/3622837 \ No newline at end of file diff --git a/data/past.txt b/data/past.txt index 6061922..0fa5928 100644 --- a/data/past.txt +++ b/data/past.txt @@ -4,4 +4,5 @@ https://doi.org/10.1145/3656456 https://doi.org/10.1145/3622828 https://doi.org/10.1145/3632882 https://doi.org/10.1145/3607862 -https://doi.org/10.1145/3586038 \ No newline at end of file +https://doi.org/10.1145/3586038 +https://doi.org/10.1145/3622837 \ No newline at end of file diff --git a/docs/index.md b/docs/index.md index 0569dd1..262b8d1 100644 --- a/docs/index.md +++ b/docs/index.md @@ -28,7 +28,7 @@ Our tools for paper selection: [plgroup on Github](https://github.com/the-au-for | 3. | September 13 | Polymorphic Type Inference for Dynamic Languages | | 4. | September 20 | A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized | | 5. | September 27 | Fat Pointers for Temporal Memory Safety of C | -| 6. | October 4 | Paper 6 discussion | +| 6. | October 4 | A Pretty Expressive Printer | | 7. | October 11 | Paper 7 discussion | | 8. | October 18 | Paper 8 discussion | | 9. | October 25 | Paper 9 discussion | diff --git a/docs/papers.md b/docs/papers.md index b6cea30..a86741d 100644 --- a/docs/papers.md +++ b/docs/papers.md @@ -2,4 +2,5 @@ 2. Lee, Edward, and Ondřej Lhoták. “Simple Reference Immutability for System F <:” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2, Oct. 2023, pp. 857–81. Crossref, https://doi.org/10.1145/3622828. 3. Castagna, Giuseppe, et al. “Polymorphic Type Inference for Dynamic Languages.” Proceedings of the ACM on Programming Languages, vol. 8, no. POPL, Jan. 2024, pp. 1179–210. Crossref, https://doi.org/10.1145/3632882. 4. Abel, Andreas, et al. “A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized.” Proceedings of the ACM on Programming Languages, vol. 7, no. ICFP, Aug. 2023, pp. 920–54. Crossref, https://doi.org/10.1145/3607862. -5. Zhou, Jie, et al. “Fat Pointers for Temporal Memory Safety of C.” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA1, Apr. 2023, pp. 316–47. Crossref, https://doi.org/10.1145/3586038. \ No newline at end of file +5. Zhou, Jie, et al. “Fat Pointers for Temporal Memory Safety of C.” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA1, Apr. 2023, pp. 316–47. Crossref, https://doi.org/10.1145/3586038. +6. Porncharoenwase, Sorawee, et al. “A Pretty Expressive Printer.” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2, Oct. 2023, pp. 1122–49. Crossref, https://doi.org/10.1145/3622837. \ No newline at end of file