Difference between revisions of "Applications"

From The Maude System
Jump to: navigation, search
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],
+
* 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://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]).

Revision as of 19:50, 20 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, IBM’s CCA, and PCKS#11, using unification and symbolic reachability. Tamarin uses Maude’s unification and has analyzed many important protocols like 5G-AKA.
  • Network protocols: AER/NCA active networks, MANETS, BGP; DDoS-Intruder models; and DDoS protection: ASV, Stable Availability, VoIP-SIP, using Maude’s statistical model checking (SMC) tool.
  • 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.
  • 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.