From The Maude System
Revision as of 20:44, 20 December 2020 by Malaga (Talk | contribs)

Jump to: navigation, search

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 (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, e.g., \cite{DBLP:conf/fm/BaeOM14}, and distributed control of airplane maneuvers \cite{DBLP:journals/corr/abs-1301-0038}.