Difference between revisions of "Applications"
From The Maude System
| Line 1: | Line 1: | ||
Maude and its formal tools have been used in many pioneering applications: | Maude and its formal tools have been used in many pioneering applications: | ||
| − | * Formal definition and verification of programming and hardware, resp. software, modeling languages: full C ([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), Java ([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), JVM ([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), [https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] ([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), Verilog ([https://ieeexplore.ieee.org/document/5558634 MKMR10]), E-LOTOS ([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], [https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), UML ([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], [https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), MOF ([https://doi.org/10.1007/s00165-009-0140-9 BM10]), ODP ([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], [https://doi.org/10.1016/j.csi.2004.10.008 DRV05], [https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), AADL ([https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), Ptolemy ([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), and BPMN ([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], [https://doi.org/10.1016/j.scico.2018.08.007 DRS18]) | + | * Formal definition and verification of programming and hardware, resp. software, modeling languages: full C ([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), Java ([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), JVM ([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), [https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] ([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), Verilog ([https://ieeexplore.ieee.org/document/5558634 MKMR10]), E-LOTOS ([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], [https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), UML ([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], [https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), MOF ([https://doi.org/10.1007/s00165-009-0140-9 BM10]), ODP ([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], [https://doi.org/10.1016/j.csi.2004.10.008 DRV05], [https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), AADL ([https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), Ptolemy ([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), and BPMN ([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], [https://doi.org/10.1016/j.scico.2018.08.007 DRS18]). |
| + | |||
| + | * Semantics of hardware architectures: MCA ARMv8 architecture([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). | ||
* Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and design and verification of the secure-by-construction Illinois’s IBOS browser ([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], [https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]). | * Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and design and verification of the secure-by-construction Illinois’s IBOS browser ([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], [https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]). | ||
| Line 23: | Line 25: | ||
* Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf TOSEM 2022]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 TASE 2021]). | * Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf TOSEM 2022]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 TASE 2021]). | ||
| − | * IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 CCS 19]). | + | * IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 CCS 19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21] TOOLS 2019). |
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es. | Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es. | ||
Revision as of 12:23, 10 March 2022
Maude and its formal tools have been used in many pioneering applications:
- Formal definition and verification of programming and hardware, resp. software, modeling languages: full C (ER12), Java (FCMR04), JVM (FMR04), NASA’s PLEXIL (RCMS12), Verilog (MKMR10), E-LOTOS (V02, VM05), UML (CE06, DRMA14), MOF (BM10), ODP (DV03, DRV05, RVD07), AADL (BOM14), Ptolemy (BOFLT14), and BPMN (DS17, DRS18).
- Semantics of hardware architectures: MCA ARMv8 architecture(XZ22).
- Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer (CMSWW07), and design and verification of the secure-by-construction Illinois’s IBOS browser (SKMT12, SMR20).
- Cryptographic protocol analysis: Maude-NPA has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM (GAEMM18), IBM’s CCA (GSEMM14), and PCKS#11 (GSEMM15), using unification and symbolic reachability. Tamarin at ETH, resp. AKISS at INRIA, use Maude’s unification to analyze protocols like 5G-AKA (DC18), resp. RFID (GK17).
- Network protocols: AER/NCA active networks (OKMTZ06), MANETS (LOM16), BGP (Wetal13, Wetal11, WTGLS12); DDoS-Intruder models; and DDoS protection (LDFN18): ASV (AMG09), Stable Availability (EMMW12), VoIP-SIP (SASGM09), using Maude’s statistical model checking (SMC) tool.
- Cloud transaction system formalization and analysis: Cassandra (LNGRG15), Google’s Megastore (GO14), P-Store (O17), etc. (Betal18), using SMC.
- Analysis of real-time and cyber-physical systems: CASH scheduling (OC06), sensor (OT09) and MANET (LOM16) networks, timed security protocols (AEMMS20), PALS transformation from synchronous to correct distributed real-time systems (MO12, BMO12) enables model checking of complex models such as AADL and Ptolemy models (BOM14) and distributed control of airplane maneuvers (BKMO12).
- Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. (Pathway Logic)
- Specification and analysis of models of Concurrency: Petri Nets (SMO01), CCS, pi-Calculus (S00), Actors (M93), REO (MSA), Orc (AM15).
- Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube (SM04), linear logic (MM02), modal logics (OPR18), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive (DM12, DMR20) and Reachability Logic (SSM17), theorem provers, HOL-to-Nuprl translator (NSM01), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.
- Networking security: N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures (CSF 2022).
- Distributed databases: SNOW-Optimal Read Atomic Transactions (TOSEM 2022), Replicated RAMP Transactions (TASE 2021).
- IoT systems: Attack Surface of Trigger-Action IoT Platforms (CCS 19), Automated Composition, Analysis and Deployment of IoT Applications ([1] TOOLS 2019).
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.
