Symbolic Parallel Composition for Multi-language Protocol Verification

• URL: http://arxiv.org/abs/2504.06833v1
• Date: Wed, 09 Apr 2025 12:50:03 GMT
• Title: Symbolic Parallel Composition for Multi-language Protocol Verification
• Authors: Faezeh Nasrabadi, Robert Künnemann, Hamed Nemati,
• Abstract summary: Security protocols often combine different languages. This practice poses a challenge to traditional verification techniques.<n>We establish principles for combining multiple programming languages operating on different atomic types using a symbolic execution semantics.
• Score: 6.514727189942011
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The implementation of security protocols often combines different languages. This practice, however, poses a challenge to traditional verification techniques, which typically assume a single-language environment and, therefore, are insufficient to handle challenges presented by the interplay of different languages. To address this issue, we establish principles for combining multiple programming languages operating on different atomic types using a symbolic execution semantics. This facilitates the (parallel) composition of labeled transition systems, improving the analysis of complex systems by streamlining communication between diverse programming languages. By treating the Dolev-Yao (DY) model as a symbolic abstraction, our approach eliminates the need for translation between different base types, such as bitstrings and DY terms. Our technique provides a foundation for securing interactions in multi-language environments, enhancing program verification and system analysis in complex, interconnected systems.

Related papers

• Exploring syntactic information in sentence embeddings through multilingual subject-verb agreement [1.4335183427838039]
  We take the approach of developing curated synthetic data on a large scale, with specific properties.<n>We use a new multiple-choice task and datasets, Blackbird Language Matrices, to focus on a specific grammatical structural phenomenon.<n>We show that despite having been trained on multilingual texts in a consistent manner, multilingual pretrained language models have language-specific differences.
  arXiv  Detail & Related papers  (2024-09-10T14:58:55Z)
• A Joint Learning Model with Variational Interaction for Multilingual Program Translation [10.77747590700758]
  Variational Interaction for Program Translation(VIM-PT) is a generative approach that jointly trains a unified model for multilingual program translation across languages. VIM-PT disentangles code into language-shared and language-specific features, using variational inference and interaction information with a novel lower bound, then achieves program translation through conditional generation.
  arXiv  Detail & Related papers  (2024-08-25T11:33:52Z)
• Interpretability of Language Models via Task Spaces [14.543168558734001]
  We present an alternative approach to interpret language models (LMs) We focus on the quality of LM processing, with a focus on their language abilities. We construct 'linguistic task spaces' that shed light on the connections LMs draw between language phenomena.
  arXiv  Detail & Related papers  (2024-06-10T16:34:30Z)
• AdaCCD: Adaptive Semantic Contrasts Discovery Based Cross Lingual Adaptation for Code Clone Detection [69.79627042058048]
  AdaCCD is a novel cross-lingual adaptation method that can detect cloned codes in a new language without annotations in that language. We evaluate the cross-lingual adaptation results of AdaCCD by constructing a multilingual code clone detection benchmark consisting of 5 programming languages.
  arXiv  Detail & Related papers  (2023-11-13T12:20:48Z)
• LAE: Language-Aware Encoder for Monolingual and Multilingual ASR [87.74794847245536]
  A novel language-aware encoder (LAE) architecture is proposed to handle both situations by disentangling language-specific information. Experiments conducted on Mandarin-English code-switched speech suggest that the proposed LAE is capable of discriminating different languages in frame-level.
  arXiv  Detail & Related papers  (2022-06-05T04:03:12Z)
• Multi-level Contrastive Learning for Cross-lingual Spoken Language Understanding [90.87454350016121]
  We develop novel code-switching schemes to generate hard negative examples for contrastive learning at all levels. We develop a label-aware joint model to leverage label semantics for cross-lingual knowledge transfer.
  arXiv  Detail & Related papers  (2022-05-07T13:44:28Z)
• Reducing language context confusion for end-to-end code-switching automatic speech recognition [50.89821865949395]
  We propose a language-related attention mechanism to reduce multilingual context confusion for the E2E code-switching ASR model. By calculating the respective attention of multiple languages, our method can efficiently transfer language knowledge from rich monolingual data.
  arXiv  Detail & Related papers  (2022-01-28T14:39:29Z)
• Cross-Lingual Adaptation for Type Inference [29.234418962960905]
  We propose a cross-lingual adaptation framework, PLATO, to transfer a deep learning-based type inference procedure across weakly typed languages. By leveraging data from strongly typed languages, PLATO improves the perplexity of the backbone cross-programming-language model.
  arXiv  Detail & Related papers  (2021-07-01T00:20:24Z)
• Unsupervised Word Translation Pairing using Refinement based Point Set Registration [8.568050813210823]
  Cross-lingual alignment of word embeddings play an important role in knowledge transfer across languages. Current unsupervised approaches rely on similarities in geometric structure of word embedding spaces across languages. This paper proposes BioSpere, a novel framework for unsupervised mapping of bi-lingual word embeddings onto a shared vector space.
  arXiv  Detail & Related papers  (2020-11-26T09:51:29Z)
• Multi-channel Transformers for Multi-articulatory Sign Language Translation [59.38247587308604]
  We tackle the multi-articulatory sign language translation task and propose a novel multi-channel transformer architecture. The proposed architecture allows both the inter and intra contextual relationships between different sign articulators to be modelled within the transformer network itself.
  arXiv  Detail & Related papers  (2020-09-01T09:10:55Z)
• Bridging Linguistic Typology and Multilingual Machine Translation with Multi-View Language Representations [83.27475281544868]
  We use singular vector canonical correlation analysis to study what kind of information is induced from each source. We observe that our representations embed typology and strengthen correlations with language relationships. We then take advantage of our multi-view language vector space for multilingual machine translation, where we achieve competitive overall translation accuracy.
  arXiv  Detail & Related papers  (2020-04-30T16:25:39Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.