Difference between revisions of "Applications"

From The Maude System
Jump to: navigation, search
(26 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:  
+
* 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]).  
[https://dl.acm.org/doi/10.1145/2103621.2103719 full C],  
+
 
[https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 Java],  
+
* 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]).
[https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 JVM],  
+
 
[https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL],  
+
* 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. [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]).
[https://ieeexplore.ieee.org/document/5558634 Verilog],  
+
 
[https://link.springer.com/article/10.1007/s10703-005-2254-x E-LOTOS], UML, MOF,
+
* Network protocols: 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].
[https://link.springer.com/chapter/10.1007/978-3-642-13464-7_5 AADL], and
+
 
[https://link.springer.com/chapter/10.1007/978-3-642-10373-5_37 Ptolemy].  
+
* 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.
* Browser security:  
+
 
[https://ieeexplore.ieee.org/abstract/document/4223215 uncovering 12 kinds of unknown attacks on Internet Explorer], and  
+
* 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]).
design and verification of the secure-by-construction Illinois’s  
+
 
[https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 IBOS browser].
+
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic])
* 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],  
+
* 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]).
[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].
+
 
* 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].
+
* 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.
* Cloud transaction system formalization and analysis: Cassandra, Google’s Megastore, P-Store, etc., using SMC.
+
 
* 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.
+
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.
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc.
+
* 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.
+

Revision as of 16:08, 22 December 2020

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

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

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.