Difference between revisions of "Applications"
From The Maude System
Line 5: | Line 5: | ||
* 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]). | ||
− | * 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], resp. [https://github.com/akiss/akiss AKISS], 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]). | + | * 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], resp. [https://github.com/akiss/akiss AKISS], 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]). |
− | * 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 ([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, 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 | + | * 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. |
− | + | ||
− | + | * 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:11, 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 (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).
- Network protocols: AER/NCA active networks (OKMTZ06), MANETS (LOM16), BGP ***ask Carolyn!***; DDoS-Intruder models; and DDoS protection: ASV (AMG09), Stable Availability (EMMW12), VoIP-SIP (SASGM09), using 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.
- 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}.