Difference between revisions of "Applications"

From The Maude System
Jump to: navigation, search
Line 9: Line 9:
 
* 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 ***ask Carolyn!***; DDoS-Intruder models; and DDoS protection: 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].
 
* 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 ***ask Carolyn!***; DDoS-Intruder models; and DDoS protection: 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].
  
* Cloud transaction system formalization and analysis: Cassandra \cite{DBLP:journals/lites/LiuGRNGM17}, Google’s Megastore \cite{DBLP:conf/sefm/GrovO14}, P-Store \cite{DBLP:conf/wadt/Olveczky16}, etc. \cite{cloud-chapter}, 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://dblp.org/rec/conf/sefm/GrovO14.bib 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 Betall18]), using SMC.
  
 
* Analysis of real-time and cyber-physical systems: CASH scheduling \cite{cash-web}, sensor \cite{OlveczkyT09} and MANET \cite{liu-etal-MANETS-JLAMP} networks, timed security protocols \cite{DBLP:conf/indocrypt/Aparicio-Sanchez20}, PALS transformation from synchronous to correct distributed real-time systems  \cite{DBLP:journals/tcs/MeseguerO12, multirate-pals-SCP}enables model checking of complex models such as AADL and Ptolemy models, e.g., \cite{DBLP:conf/fm/BaeOM14}, and distributed control of airplane maneuvers \cite{DBLP:journals/corr/abs-1301-0038}.
 
* Analysis of real-time and cyber-physical systems: CASH scheduling \cite{cash-web}, sensor \cite{OlveczkyT09} and MANET \cite{liu-etal-MANETS-JLAMP} networks, timed security protocols \cite{DBLP:conf/indocrypt/Aparicio-Sanchez20}, PALS transformation from synchronous to correct distributed real-time systems  \cite{DBLP:journals/tcs/MeseguerO12, multirate-pals-SCP}enables model checking of complex models such as AADL and Ptolemy models, e.g., \cite{DBLP:conf/fm/BaeOM14}, and distributed control of airplane maneuvers \cite{DBLP:journals/corr/abs-1301-0038}.

Revision as of 20:18, 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 (GAEMM18), IBM’s CCA (GSEMM14), and PCKS#11 (GSEMM15), using unification and symbolic reachability. Tamarin, resp. AKISS, 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. (Betall18), using SMC.
  • Analysis of real-time and cyber-physical systems: CASH scheduling \cite{cash-web}, sensor \cite{OlveczkyT09} and MANET \cite{liu-etal-MANETS-JLAMP} networks, timed security protocols \cite{DBLP:conf/indocrypt/Aparicio-Sanchez20}, PALS transformation from synchronous to correct distributed real-time systems \cite{DBLP:journals/tcs/MeseguerO12, multirate-pals-SCP}enables model checking of complex models such as AADL and Ptolemy models, e.g., \cite{DBLP:conf/fm/BaeOM14}, and distributed control of airplane maneuvers \cite{DBLP:journals/corr/abs-1301-0038}.