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: | + | * Formal definition and verification of programming and hardware, resp. software, modeling languages: full C |
| − | full C | + | |
([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), | ([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), | ||
Java | Java | ||
| Line 44: | Line 43: | ||
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). | * Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). | ||
| − | * Browser security: | + | * Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and |
| − | 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 | 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/978-3-642-35861-6_14 SKMT12], | ||
| Line 63: | Line 61: | ||
Secure bandwidth reservation in path-aware Internet architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]), | Secure bandwidth reservation in path-aware Internet architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]), | ||
end-to-end name resolution ([https://dl.acm.org/doi/abs/10.1145/3603269.3604870 LDHBVBP23]). | end-to-end name resolution ([https://dl.acm.org/doi/abs/10.1145/3603269.3604870 LDHBVBP23]). | ||
| − | SCION’s bandwidth allocation protocol ([https://link.springer.com/book/10.1007/978-3-031-05288-0 CLBHHMP22]. | + | SCION’s bandwidth allocation protocol ([https://link.springer.com/book/10.1007/978-3-031-05288-0 CLBHHMP22]). |
* Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC. | * Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC. | ||
Revision as of 13:58, 20 March 2024
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 (OBM10, BOM14), Ptolemy (BOFLT14), BPMN (DS17, DRS18, DMC23, DPR24), DSMLs (RRDV, RDV09, D23), Multi-Level Modelling Languages (RMDRW23, RDK23).
- 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. See EMM09. An account of the NRL protocol analyzer can be found here. Tamarin at ETH, resp. AKISS at INRIA, use Maude’s unification to analyze protocols like 5G-AKA (DC18), resp. RFID (GK17).
- Networks:
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. Secure bandwidth reservation in path-aware Internet architectures (WLSPB22), end-to-end name resolution (LDHBVBP23). SCION’s bandwidth allocation protocol (CLBHHMP22).
- 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). See EKLLMS02.
- 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.
- Distributed databases: SNOW-Optimal Read Atomic Transactions (L22), Replicated RAMP Transactions (LL21).
- IoT systems: Attack Surface of Trigger-Action IoT Platforms (WDYLBG19), Automated Composition, Analysis and Deployment of IoT Applications (DG19).
- Runtime verification: See works by Roşu and Havelund.
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.
