Difference between revisions of "Applications"

From The Maude System
Jump to: navigation, search
 
(40 intermediate revisions by the same user not shown)
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]),  
+
* 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-642-13464-7_5 OBM10], [https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), Ptolemy ([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), BPMN ([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], [https://doi.org/10.1016/j.scico.2018.08.007 DRS18], [https://doi.org/10.1007/978-3-031-12441-9_6 DMC23], [https://doi.org/10.1016/j.jlamp.2023.100928 DPR24]), DSMLs ([https://doi.org/10.5381/jot.2007.6.9.a10 RRDV], [https://doi.org/10.1177/0037549709341635 RDV09], [https://doi.org/10.5381/jot.2022.21.4.a2 D23]), Multi-Level Modelling Languages ([https://doi.org/10.1016/j.jlamp.2022.100831 RMDRW23], [https://doi.org/10.1007/s10270-021-00947-1 RDK23]).
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]),  
+
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]).  
[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]).  
+
  
 
* 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]).
  
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like [http://personales.upv.es/sanesro/Maude-NPA-YubiKey-YubiHSM/ Yubikey&YubiHSM], [https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 IBM’s CCA], and PCKS#11, using unification and symbolic reachability. [https://tamarin-prover.github.io/ Tamarin] uses Maude’s unification and has analyzed many important protocols like [https://people.cispa.io/cas.cremers/tamarin/5G/ 5G-AKA].
+
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM ([https://easychair.org/publications/paper/qkkq GAEMM18]), IBM’s CCA ([https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 GSEMM14]), and PCKS#11 ([https://link.springer.com/chapter/10.1007/978-3-319-27152-1_5 GSEMM15]), using unification and symbolic reachability. See [https://doi.org/10.1007/978-3-642-03829-7_1 EMM09]. An account of the NRL protocol analyzer can be found [https://doi.org/10.1016/j.tcs.2006.08.035 here]. [https://tamarin-prover.github.io/ Tamarin] at ETH, resp. [https://github.com/akiss/akiss AKISS] at INRIA, use Maude’s unification to analyze protocols like 5G-AKA ([https://people.cispa.io/cas.cremers/tamarin/5G/ DC18]), resp. RFID ([https://link.springer.com/chapter/10.1007/978-3-319-66399-9_1 GK17]).
* Network protocols: AER/NCA active networks, MANETS, BGP; DDoS-Intruder models; and DDoS protection: ASV, Stable Availability, VoIP-SIP, using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool].
+
 
* Cloud transaction system formalization and analysis: Cassandra, Google’s Megastore, P-Store, etc., using SMC.
+
* Networks: AER/NCA active networks ([https://link.springer.com/chapter/10.1007/3-540-45314-8_24 OKMTZ06]), MANETS ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]), BGP ([https://repository.upenn.edu/cgi/viewcontent.cgi?article=2029&context=cis_reports Wetal13], [https://link.springer.com/chapter/10.1007/978-3-642-21461-5_22 Wetal11], [https://link.springer.com/chapter/10.1007/978-3-642-28756-5_20 WTGLS12]); DDoS-Intruder models; and DDoS protection ([https://www.sciencedirect.com/science/article/pii/S2352220816301651 LDFN18]): ASV ([https://www.sciencedirect.com/science/article/pii/S1571066109000747 AMG09]), Stable Availability ([http://dx.doi.org/10.1007/978-3-642-28872-2_6 EMMW12]), VoIP-SIP ([https://link.springer.com/chapter/10.1007/978-3-642-04444-1_24 SASGM09]), using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool]. 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]). SCION’s bandwidth allocation protocol ([https://link.springer.com/book/10.1007/978-3-031-05288-0 CLBHHMP22]).
* Analysis of real-time and cyber-physical systems: CASH scheduling, sensor and MANET networks, timed security protocols, PALS transformation from synchronous to correct distributed real-time systems enables model checking of complex models such as AADL and Ptolemy models and distributed control of airplane maneuvers.
+
 
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc.
+
* 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.
* Specification and analysis of models of Concurrency: Petri Nets, CCS, pi-Calculus, Actors, REO, Orc.  
+
 
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube, linear logic, modal logics, computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive and Reachability Logic theorem provers, HOL-to-Nuprl translator, integration of logic and deep-learning, etc.  These applications use meta-level, search, and symbolic features.
+
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_7 AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]).
 +
 
 +
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]). See [https://pubmed.ncbi.nlm.nih.gov/11928493/ EKLLMS02].
 +
 
 +
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252 S00]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]).
 +
 
 +
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc.  These applications use meta-level, search, and symbolic features.
 +
 
 +
* Distributed databases: SNOW-​Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).
 +
 
 +
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).
 +
 
 +
* Runtime verification: See works by [https://doi.org/10.1007/s10515-005-6205-y 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.

Latest revision as of 14:03, 20 March 2024

Maude and its formal tools have been used in many pioneering applications:

  • 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).
  • 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).

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.