首页> 外文会议>International Conference of B and Z Users >Are Smart Cards the Ideal Domain for Applying Formal Methods?
【24h】

Are Smart Cards the Ideal Domain for Applying Formal Methods?

机译:智能卡是应用正式方法的理想域吗?

获取原文

摘要

The traditional approach for programming smart cards does not allow the creation of downloadable executable code and requires programmers with experience in programming in low-level languages. This approach, associated with a high quality qualification process, produce secured smart card. Unfortunately, it does not allow card manufacturers and issuers to quickly respond to the market changes, and it limits the flexibility of smart card applications. Open smart card programming provides a more dynamic approach to card applications. High-level languages and security mechanisms are the basis for the programming of open smart cards. Most notable efforts towards such smart card systems are Java Card [22], MultOS [14] and Smart Card for Windows [15], which provide application developers an opportunity to develop rapidly applications. The main drawback with this kind of smart card is the risk to download a hostile application that will exploit a faulty implementation module of the platform. Security is always a big concern for smart cards, but the issue is getting more intense with multi-applicative platforms and post issuance code downloading. The correct design and implementation of the system is the key to shun such an attack. Fault prevention offers different techniques to remove latent errors from the system. The fault avoidance concerns methodologies and appropriate techniques to avoid the introduction of fault during the design and the construction of the system. In a first approach, one can believe that smart card can only get benefits of using formal methods. But it remains difficult to integrate these methods in the development process.
机译:编程智能卡的传统方法不允许创建可下载的可执行代码,并要求程序员以低级别语言编程的经验。这种方法与高质量的资格过程相关,生产安全智能卡。不幸的是,它不允许卡制造商和发行人能够快速响应市场变化,并限制智能卡应用的灵活性。开放式智能卡编程为卡片应用提供了一种更具动态的方法。高级语言和安全机制是开放智能卡编程的基础。对于这种智能卡系统来说,最显着的努力是Java Card [22],MultOS [14]和Windows [15]的智能卡,它为应用程序开发人员提供了开发快速应用的机会。这种智能卡的主要缺点是下载一个敌意应用程序的风险,该应用程序将利用平台的故障实现模块。安全始终对智能卡始终是一个重要的关注,但问题正在与多应用平台和发布后码下载更加激烈。系统的正确设计和实现是避免这样的攻击的关键。故障预防提供了不同的技术来消除系统的潜在错误。故障避免涉及方法和适当的技术,以避免在设计期间引入故障和系统的构造。在第一种方法中,人们可以相信智能卡只能获得使用正式方法的好处。但它仍然难以将这些方法集成在开发过程中。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号