50干川 尚人57Naoto HOSHIKAWA住井英二郎動的機密性の環境双模倣による静的検証58Eijiro SUMIIなりすまし検出を目的としたクロック周波数信号情報のドリフト特徴に基づくディジタル機器の識別技術（2019採択）Identification technology of digital equipment based on drift characteristics of clock frequency signal information for spoof detection(Project 2019)（2019採択）Static Verificatioin of Dynamic Confidentiality by Environmental Bisimulation(Project 2019)IoT機器のオープン化は幅広く設置された機器の相互利用性を高めるため，安くて効率的なIoTサービスの提供につながり，イノベーションを促進すると言われている．一方で，オープンなIoT機器はなりすましのリスクも高める．本研究テーマはネットワークサービスを構成する安価で低性能なIoT機器でも適用可能な機器識別技術の開発である．その実現手法として，コンピュータ固有のクロック信号のずれ特性を識別子として利用する．本報告ではクロックのずれと温度の相関性に着目した特徴抽出およびその識別手法の実装と検証結果を示す．提案技術は幅広いディジタル機器で容易に実装できることから，IoTインフラに不可欠な基盤技術として期待できる．Open IoT equipment will increase the interoperability of resources across a wide range of owners, and it will facilitate the innovation of inexpensive and efficient IoT services. On the other hand, the openness of IoT equipment also increases the risk of spoofing. This research theme is the development of computer identifica-tion technology that can be used for inexpensive and low-performance IoT equipment that constitute network services. We implement it by using the drift characteristics of computer-specific clock signals as identifiers. In this report, we show the implementation and validation results of a feature extraction and identification method using the correlation between clock drift and temperature. The proposed technology can be easily im-plemented in a wide variety of digital equipment, it is useful as an indispensable basic technology for IoT in-frastructure.値やその型に機密性（値が漏洩しないこと）や完全性（値が改ざんされていないこと）を付与したセキュリティ型付きλ計算に，故意かつ必要な低機密化(declassification)の操作を導入し，その上で適切な条件付きの非干渉性(non-interference)（プログラム等価性に基づく安全性）を数理論理学的に証明するための環境双模倣(environmental bisimulation)の理論を定義した．当研究は研究代表者が綿密に指導した博士前期課程学生らとの共同研究である．当文書は学術論文ではなく研究助成の報告書であり，他の場での今後の発表を妨げない．We introduced an intentional and necessary operation of “declassification” (unclassification) into securi-ty-typed lambda-calculus with confidentiality (the property that a value does not leak) and integrity (the prop-erty that a value is not tampered) of values and their types, and defined the theory of environmental bisimula-tions to prove by mathematical logic “non-interference” (security property based on program equivalence) with appropriate conditions. This research was conducted in collaboration with masterʼs program students under intensive supervision by the principal investigator. This document is not an academic paper but is a re-port of a research grant, and does not prevent future publications in other venues.
元のページ ../index.html#54