Rubicon: Bounded Verification of Web Applications
Rubicon is a verifier for web applications. Specifications are written in an embedded domain-specific language and are checked fully automatically. Rubicon is designed to fit with current practices: its language is based on RSpec, a popular testing framework, and its analysis leverages the standard...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Association for Computing Machinery (ACM)
2014
|
| Online Access: | http://hdl.handle.net/1721.1/86919 https://orcid.org/0000-0003-4864-078X |
| _version_ | 1811076710043484160 |
|---|---|
| author | Jackson, Daniel Near, Joseph Paul |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Jackson, Daniel Near, Joseph Paul |
| author_sort | Jackson, Daniel |
| collection | MIT |
| description | Rubicon is a verifier for web applications. Specifications are written in an embedded domain-specific language and are checked fully automatically. Rubicon is designed to fit with current practices: its language is based on RSpec, a popular testing framework, and its analysis leverages the standard Ruby interpreter to perform symbolic execution (generating verification conditions that are checked by the Alloy Analyzer). Rubicon has been evaluated on five open-source applications; in one, a widely used customer relationship management system, a previously unknown security flaw was revealed. |
| first_indexed | 2024-09-23T10:26:19Z |
| format | Article |
| id | mit-1721.1/86919 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T10:26:19Z |
| publishDate | 2014 |
| publisher | Association for Computing Machinery (ACM) |
| record_format | dspace |
| spelling | mit-1721.1/869192022-09-26T17:53:51Z Rubicon: Bounded Verification of Web Applications Jackson, Daniel Near, Joseph Paul Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Near, Joseph Paul Jackson, Daniel Rubicon is a verifier for web applications. Specifications are written in an embedded domain-specific language and are checked fully automatically. Rubicon is designed to fit with current practices: its language is based on RSpec, a popular testing framework, and its analysis leverages the standard Ruby interpreter to perform symbolic execution (generating verification conditions that are checked by the Alloy Analyzer). Rubicon has been evaluated on five open-source applications; in one, a widely used customer relationship management system, a previously unknown security flaw was revealed. National Science Foundation (U.S.) (CRI: CRD - Development of Alloy Technology and Materials Grant 0707612) 2014-05-09T17:35:48Z 2014-05-09T17:35:48Z 2012-11 Article http://purl.org/eprint/type/ConferencePaper 9781450316149 http://hdl.handle.net/1721.1/86919 Joseph P. Near and Daniel Jackson. 2012. Rubicon: bounded verification of web applications. In Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering (FSE '12). ACM, New York, NY, USA, Article 60, 11 pages. https://orcid.org/0000-0003-4864-078X en_US http://dx.doi.org/10.1145/2393596.2393667 Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering (FSE '12) Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Association for Computing Machinery (ACM) MIT web domain |
| spellingShingle | Jackson, Daniel Near, Joseph Paul Rubicon: Bounded Verification of Web Applications |
| title | Rubicon: Bounded Verification of Web Applications |
| title_full | Rubicon: Bounded Verification of Web Applications |
| title_fullStr | Rubicon: Bounded Verification of Web Applications |
| title_full_unstemmed | Rubicon: Bounded Verification of Web Applications |
| title_short | Rubicon: Bounded Verification of Web Applications |
| title_sort | rubicon bounded verification of web applications |
| url | http://hdl.handle.net/1721.1/86919 https://orcid.org/0000-0003-4864-078X |
| work_keys_str_mv | AT jacksondaniel rubiconboundedverificationofwebapplications AT nearjosephpaul rubiconboundedverificationofwebapplications |