Relational Adversarial Logic

Relational Adversarial Logic | Research Square window.SnipcartSettings = { analytics: { enabled: false } }; (function() { var accessVector = localStorage.getItem('access_vector') || ''; window.dataLayer = window.dataLayer || []; if (accessVector) { window.dataLayer.push({ user: { profile: { profileInfo: { snid: accessVector } } } }); } })(); (function(w,d,s,l,i){w[l]=w[l]||[];w[l].push({'gtm.start':new Date().getTime(),event:'gtm.js'});var f=d.getElementsByTagName(s)[0],j=d.createElement(s),dl=l!='dataLayer'?'&l='+l:'';j.async=true;j.src='https://www.googletagmanager.com/gtm.js?id='+i+dl;f.parentNode.insertBefore(j,f);})(window,document,'script','dataLayer','GTM-K279D39R'); Browse Preprints In Review Journals COVID-19 Preprints AJE Video Bytes Research Tools Research Promotion AJE Professional Editing AJE Rubriq About Preprint Platform In Review Editorial Policies Our Team Advisory Board Help Center Sign In Submit a Preprint Cite Share Download PDF Research Article Relational Adversarial Logic Julien Vanegue This is a preprint; it has not been peer reviewed by a journal. https://doi.org/ 10.21203/rs.3.rs-2874730/v1 This work is licensed under a CC BY 4.0 License Status: Posted Version 1 posted You are reading this latest preprint version Abstract Adversarial Logic is an extension of Incorrectness Logic providing a formal framework to study \emph{security exploits}. This article introduces \emph{Relational Adversarial Logic} (RAL), a derived logic from AL capable of reasoning on attack proofs for software security hyper-properties. Unlike other approaches to under-approximate relational analysis, we model the relation between two comparable implementations by introducing an explicit adversarial term, which is composed in parallel to the programs under comparison. Unlike in the original Adversarial logic where the parallel composition is used to model the adversary as a saboteur, the adversarial term is used as an arbiter in RAL. As such, RAL can express relational under-approximation without introducing meta-variables or a higher level logic. We demonstrate the relational capabilities of RAL by modeling a real URL confusion vulnerability between two widespread URL parsing implementations. Our presentation demonstrates that it only suffices to introduce new derived rules from AL, rather than introducing a new logic or relying on meta-variables as done in other approaches. As such, RAL retains simplicity and is more faithful to the original incorrectness logic by O'Hearn, from which it inherits its soundness. incorrectness adversarial logic security exploit under-approximate Full Text Additional Declarations No competing interests reported. Cite Share Download PDF Status: Posted Version 1 posted You are reading this latest preprint version Research Square lets you share your work early, gain feedback from the community, and start making changes to your manuscript prior to peer review in a journal. As a division of Research Square Company, we’re committed to making research communication faster, fairer, and more useful. We do this by developing innovative software and high quality services for the global research community. Our growing team is made up of researchers and industry professionals working together to solve the most critical problems facing scientific publishing. Also discoverable on Platform About Our Team In Review Editorial Policies Advisory Board Help Center Resources Author Services Accessibility API Access RSS feed Manage Cookie Preferences © Research Square 2026 | ISSN 2693-5015 (online) Privacy Policy Terms of Service Do Not Sell My Personal Information {"props":{"pageProps":{"initialData":{"identity":"rs-2874730","acceptedTermsAndConditions":true,"allowDirectSubmit":true,"archivedVersions":[],"articleType":"Research Article","associatedPublications":[],"authors":[{"id":196185823,"identity":"cd9c0e23-5fe6-46c9-9cb8-7e5d06198155","order_by":0,"name":"Julien Vanegue","email":"data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAZAAAAAyAQMAAABI0h/eAAAABlBMVEX///8AAABVwtN+AAAACXBIWXMAAA7EAAAOxAGVKw4bAAABAElEQVRIiWNgGAWjYBACxgbmhgNIfBuQWOMB7IphWhhRtKSBxfBqASlA5h0Gk3i1MM9IbDzwcQdDYv/s5sOveSrO261tPwy0pcYmGqcdMxIbDs48w5A4486xNGueM7eTt51JBGo5lpbbgEfLYd42BmOGGzlmxrxtt5PNDgC1MDYcxq/lL1CL/I38b8a8/84lm51/SIQWxjYGOYMbOcyPeRsO2JndIGRLz8OGg71tEnKGN9LMGOccS04wuwG0JQGPXwzbkw9/+NlmwyN3I/nxhzc1dvZm59MfPvhQY4NbC0RCAkSwgchEsEACDuUgII/EZv4AJOzxKB4Fo2AUjIIRCgA6Jmmssj1GMQAAAABJRU5ErkJggg==","orcid":"","institution":"Bloomberg (United States)","correspondingAuthor":true,"submittingAuthor":false,"prefix":"","firstName":"Julien","middleName":"","lastName":"Vanegue","suffix":""}],"badges":[],"createdAt":"2023-04-28 23:29:10","currentVersionCode":1,"declarations":"","doi":"10.21203/rs.3.rs-2874730/v1","doiUrl":"https://doi.org/10.21203/rs.3.rs-2874730/v1","draftVersion":[],"editorialEvents":[],"editorialNote":"","failedWorkflow":false,"files":[{"id":50480552,"identity":"ff9fbac5-a27c-4a73-9277-11375bbb1827","added_by":"auto","created_at":"2024-02-01 07:44:58","extension":"pdf","order_by":1,"title":"","display":"","copyAsset":false,"role":"manuscript-pdf","size":387124,"visible":true,"origin":"","legend":"","description":"","filename":"b78a9c5411ff45a29a4e37cd3440a974.pdf","url":"https://assets-eu.researchsquare.com/files/rs-2874730/v1_covered_2aa21b83-a44c-4cd9-a20c-f595d4bf8ce1.pdf"}],"financialInterests":"No competing interests reported.","formattedTitle":"Relational Adversarial Logic","fulltext":[],"fulltextSource":"","fullText":"","funders":[],"hasAdminPriorityOnWorkflow":false,"hasManuscriptDocX":false,"hasOptedInToPreprint":true,"hasPassedJournalQc":"","hasAnyPriority":false,"hideJournal":true,"highlight":"","institution":"","isAcceptedByJournal":false,"isAuthorSuppliedPdf":true,"isDeskRejected":"","isHiddenFromSearch":false,"isInQc":false,"isInWorkflow":false,"isPdf":true,"isPdfUpToDate":true,"isWithdrawnOrRetracted":false,"journal":{"display":true,"email":"[email protected]","identity":"researchsquare","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":true,"externalIdentity":"","sideBox":"","snPcode":"","submissionUrl":"/submission","title":"Research Square","twitterHandle":"researchsquare","acdcEnabled":true,"dfaEnabled":false,"editorialSystem":"","reportingPortfolio":"","inReviewEnabled":false,"inReviewRevisionsEnabled":true},"keywords":"incorrectness, adversarial, logic, security, exploit, under-approximate","lastPublishedDoi":"10.21203/rs.3.rs-2874730/v1","lastPublishedDoiUrl":"https://doi.org/10.21203/rs.3.rs-2874730/v1","license":{"name":"CC BY 4.0","url":"https://creativecommons.org/licenses/by/4.0/"},"manuscriptAbstract":"Adversarial Logic is an extension of Incorrectness Logic providing a formal framework to study \\emph{security exploits}. This article introduces \\emph{Relational Adversarial Logic} (RAL), a derived logic from AL capable of reasoning on attack proofs for software security hyper-properties. Unlike other approaches to under-approximate relational analysis, we model the relation between two comparable implementations by introducing an explicit adversarial term, which is composed in parallel to the programs under comparison. Unlike in the original Adversarial logic where the parallel composition is used to model the adversary as a saboteur, the adversarial term is used as an arbiter in RAL. As such, RAL can express relational under-approximation without introducing meta-variables or a higher level logic. We demonstrate the relational capabilities of RAL by modeling a real URL confusion vulnerability between two widespread URL parsing implementations. Our presentation demonstrates that it only suffices to introduce new derived rules from AL, rather than introducing a new logic or relying on meta-variables as done in other approaches. As such, RAL retains simplicity and is more faithful to the original incorrectness logic by O'Hearn, from which it inherits its soundness.","manuscriptTitle":"Relational Adversarial Logic","msid":"","msnumber":"","nonDraftVersions":[{"code":1,"date":"2023-05-03 03:39:51","doi":"10.21203/rs.3.rs-2874730/v1","editorialEvents":[{"type":"communityComments","content":0}],"status":"published","journal":{"display":true,"email":"[email protected]","identity":"researchsquare","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":true,"externalIdentity":"","sideBox":"","snPcode":"","submissionUrl":"/submission","title":"Research Square","twitterHandle":"researchsquare","acdcEnabled":true,"dfaEnabled":false,"editorialSystem":"","reportingPortfolio":"","inReviewEnabled":false,"inReviewRevisionsEnabled":true}}],"origin":"","ownerIdentity":"7d28bc33-b6c4-4724-9825-caca2780d204","owner":[],"postedDate":"May 3rd, 2023","published":true,"recentEditorialEvents":[],"rejectedJournal":[],"revision":"","amendment":"","status":"posted","subjectAreas":[],"tags":[],"updatedAt":"2024-02-01T07:36:48+00:00","versionOfRecord":[],"versionCreatedAt":"2023-05-03 03:39:51","video":"","vorDoi":"","vorDoiUrl":"","workflowStages":[]},"version":"v1","identity":"rs-2874730","journalConfig":"researchsquare"},"__N_SSP":true},"page":"/article/[identity]/[[...version]]","query":{"redirect":"/article/rs-2874730","identity":"rs-2874730","version":["v1"]},"buildId":"WrCJVZZCHTDjtuVLN7oU0","isFallback":false,"isExperimentalCompile":false,"dynamicIds":[84888],"gssp":true,"scriptLoader":[]}