Difference between revisions of "Applications"
From The Maude System
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]), |
− | 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]), | 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]), | JVM ([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), | ||
Line 16: | Line 15: | ||
BPMN ([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], | 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.1016/j.scico.2018.08.007 DRS18]). | ||
− | * Browser security: [https://ieeexplore.ieee.org/abstract/document/4223215 | + | |
+ | * 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 [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]. | ||
* 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]. | * 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]. |
Revision as of 19:48, 20 December 2020
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 (ER12),
Java (FCMR04), JVM (FMR04), NASA’s PLEXIL (RCMS12), Verilog (MKMR10), E-LOTOS (V02, VM05), UML (CE06, DRMA14), MOF (BM10), ODP (DV03, DRV05, RVD07), AADL (BOM14), Ptolemy (BOFLT14), and BPMN (DS17, DRS18).
- 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.