Fetching the paper…

Reading the bibliography…

2024

3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers

Fakhoury, Sarah, Kuppe, Markus, Lahiri, Shuvendu K. et al.

Original
PDF
Post on X

Understand

Improper parsing of attacker-controlled input is a leading source of software security vulnerabilities, especially when programmers transcribe informal format descriptions in RFCs into efficient parsing logic in low-level, memory unsafe languages.

Several researchers have proposed formal specification languages for data formats from which efficient code can be extracted.
However, distilling informal requirements into formal specifications is challenging and, despite their benefits, new, formal languages are hard for people to learn and use.
In this work, we present 3DGen, a framework that makes use of AI agents to transform mixed informal input, including natural language documents (i.e., RFCs) and example inputs into format specifications in a language called 3D.

3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers · Around

Built on

Z. Manna and R. Waldinger, “A deductive approach to program synthesis,” ACM Trans. Program. Lang. Syst. , vol. 2, no. 1, p. 90–121, jan 1980. [Online]. Available: https://doi.org/10.1145/357084.357090
1980
Earlier work this paper cites.
L. De Moura and N. Bjørner, “Z3: An efficient smt solver,” in Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings 14 . Springer, 2008, pp. 337–340
2008
Earlier work this paper cites.
R. Alur, R. Bodík, G. Juniwal, M. M. K. Martin, M. Raghothaman, S. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa, “Syntax-guided synthesis,” in Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013 . IEEE, 2013, pp. 1–8. [Online]. Available: https://ieeexplore.ieee.org/document/6679385/
2013
Earlier work this paper cites.
J. Bangert and N. Zeldovich, “Nail: A practical tool for parsing and generating data formats,” in 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14) . Broomfield, CO: USENIX Association, Oct. 2014, pp. 615–628. [Online]. Available: https://www.usenix.org/conference/osdi14/technical-sessions/presentation/bangert
2014
Earlier work this paper cites.
C. Barrett, P. Fontaine, and C. Tinelli, “The Satisfiability Modulo Theories Library (SMT-LIB),” https://smtlib.cs.uiowa.edu/ , 2016
2016
Earlier work this paper cites.
J. Protzenko, J.-K. Zinzindohoué, A. Rastogi, T. Ramananandro, P. Wang, S. Zanella-Béguelin, A. Delignat-Lavaud, C. Hritcu, K. Bhargavan, C. Fournet, and N. Swamy, “Verified low-level programming embedded in F*,” PACMPL , vol. 1, no. ICFP, pp. 17:1–17:29, Sep. 2017. [Online]. Available: http://arxiv.org/abs/1703.00053
Original
2017
Earlier work this paper cites.
S. Gulwani, O. Polozov, and R. Singh, “Program synthesis,” Found. Trends Program. Lang. , vol. 4, no. 1-2, pp. 1–119, 2017. [Online]. Available: https://doi.org/10.1561/2500000010
2017
Earlier work this paper cites.
T. Ramananandro, A. Delignat-Lavaud, C. Fournet, N. Swamy, T. Chajed, N. Kobeissi, and J. Protzenko, “Everparse: Verified secure zero-copy parsers for authenticated message formats,” in Proceedings of the 28th USENIX Conference on Security Symposium , ser. SEC’19. USA: USENIX Association, 2019, p. 1465–1482
2019
Earlier work this paper cites.
M. Chen, J. Tworek, H. Jun, Q. Yuan, H. P. d. O. Pinto, J. Kaplan, H. Edwards, Y. Burda, N. Joseph, G. Brockman et al. , “Evaluating large language models trained on code,” arXiv preprint arXiv:2107.03374 , 2021
Original
2021
Earlier work this paper cites.

Similar

J. Austin, A. Odena, M. Nye, M. Bosma, H. Michalewski, D. Dohan, E. Jiang, C. Cai, M. Terry, Q. Le et al. , “Program synthesis with large language models,” arXiv preprint arXiv:2108.07732 , 2021
Original
2021
Cited alongside, same era.
J. Yen, T. Lévai, Q. Ye, X. Ren, R. Govindan, and B. Raghavan, “Semi-automated protocol disambiguation and code generation,” in Proceedings of the 2021 ACM SIGCOMM 2021 Conference , ser. SIGCOMM ’21. New York, NY, USA: Association for Computing Machinery, 2021, p. 272–286. [Online]. Available: https://doi.org/10.1145/3452296.3472910
2021
Cited alongside, same era.
N. Swamy, T. Ramananandro, A. Rastogi, I. Spiridonova, H. Ni, D. Malloy, J. Vazquez, M. Tang, O. Cardona, and A. Gupta, “Hardening attack surfaces with formally proven binary format parsers,” in Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’22), June 13–17, 2022, San Diego, CA, USA , 2022. [Online]. Available: https://www.fstar-lang.org/papers/EverParse3D.pdf
2022
Cited alongside, same era.

Then

Z. Xi, W. Chen, X. Guo, W. He, Y. Ding, B. Hong, M. Zhang, J. Wang, S. Jin, E. Zhou et al. , “The rise and potential of large language model based agents: A survey,” arXiv preprint arXiv:2309.07864 , 2023
Original
2023
Later among the works it cites.
L. Wang, C. Ma, X. Feng, Z. Zhang, H. Yang, J. Zhang, Z. Chen, J. Tang, X. Chen, Y. Lin et al. , “A survey on large language model based autonomous agents,” arXiv preprint arXiv:2308.11432 , 2023
Original
2023
Later among the works it cites.
Y. Du, S. Li, A. Torralba, J. B. Tenenbaum, and I. Mordatch, “Improving factuality and reasoning in language models through multiagent debate,” arXiv preprint arXiv:2305.14325 , 2023
Original
2023
Later among the works it cites.
C. Qian, X. Cong, C. Yang, W. Chen, Y. Su, J. Xu, Z. Liu, and M. Sun, “Communicative agents for software development,” arXiv preprint arXiv:2307.07924 , 2023
Original
2023
Later among the works it cites.

Beyond the bibliography

alphaXiv searches the wider corpus for related work and actual follow-ups.

Open on alphaXiv

alphaXiv is searching for related work…

S. Yao, J. Zhao, D. Yu, N. Du, I. Shafran, K. Narasimhan, and Y. Cao, “React: Synergizing reasoning and acting in language models,” arXiv preprint arXiv:2210.03629 , 2022

2022

Cited alongside, same era.

H. Pearce, B. Ahmad, B. Tan, B. Dolan-Gavitt, and R. Karri, “Asleep at the keyboard? assessing the security of github copilot’s code contributions,” in 2022 IEEE Symposium on Security and Privacy (SP) , 2022, pp. 754–768

2022

Cited alongside, same era.

Y. Li, D. Choi, J. Chung, N. Kushman, J. Schrittwieser, R. Leblond, T. Eccles, J. Keeling, F. Gimeno, A. D. Lago, T. Hubert, P. Choy, C. d. M. d’Autume, I. Babuschkin, X. Chen, P.-S. Huang, J. Welbl, S. Gowal, A. Cherepanov, J. Molloy, D. J. Mankowitz, E. S. Robson, P. Kohli, N. de Freitas, K. Kavukcuoglu, and O. Vinyals, “Competition-level code generation with alphacode,” 2022. [Online]. Available: https://arxiv.org/abs/2203.07814

2022

Cited alongside, same era.

B. Chen, F. Zhang, A. Nguyen, D. Zan, Z. Lin, J.-G. Lou, and W. Chen, “Codet: Code generation with generated tests,” 2022. [Online]. Available: https://arxiv.org/abs/2207.10397

2022

Cited alongside, same era.

OpenAI, “Gpt-4 technical report,” 2023

2023

Cited alongside, same era.

Y. Gao, Y. Xiong, X. Gao, K. Jia, J. Pan, Y. Bi, Y. Dai, J. Sun, and H. Wang, “Retrieval-augmented generation for large language models: A survey,” arXiv preprint arXiv:2312.10997 , 2023

2023

Cited alongside, same era.

Q. Wu, G. Bansal, J. Zhang, Y. Wu, S. Zhang, E. Zhu, B. Li, L. Jiang, X. Zhang, and C. Wang, “Autogen: Enabling next-gen llm applications via multi-agent conversation framework,” arXiv preprint arXiv:2308.08155 , 2023

2023

Later among the works it cites.

A. Gandhi, T. Q. Nguyen, H. Jiao, R. Steen, and A. Bhatawdekar, “Natural language commanding via program synthesis,” 2023

2023

Later among the works it cites.

S. K. Lahiri, S. Fakhoury, A. Naik, G. Sakkas, S. Chakraborty, M. Musuvathi, P. Choudhury, C. von Veh, J. P. Inala, C. Wang, and J. Gao, “Interactive code generation via test-driven user-intent formalization,” CoRR , vol. abs/2208.05950, 2023. [Online]. Available: https://doi.org/10.48550/arXiv.2208.05950

2023

Later among the works it cites.

M. Endres, S. Fakhoury, S. Chakraborty, and S. K. Lahiri, “Formalizing natural language intent into program specifications via large language models,” CoRR , vol. abs/2310.01831, 2023. [Online]. Available: https://doi.org/10.48550/arXiv.2310.01831

2023

Later among the works it cites.

M. Md Rakib Hossain Misu, C. V. Lopes, I. Ma, and J. Noble, “Towards ai-assisted synthesis of verified dafny methods,” 2024

2024

Closest in time.