Updated on 2025/02/27

写真a

 
TOMOISHI Masahiko
 
Organization
Center for Information Infrastructure Professor
Title
Professor
External link

Degree

  • 工学修士 ( 東京工業大学 )

Research Interests

  • ソフトウェア工学

  • 情報セキュリティ

  • 情報ネットワーク

  • 時間論理

  • 情報ネットワーク、情報セキュリティ、ソフトウェア工学

Research Areas

  • Informatics / Information network

  • Informatics / Software

  • Informatics / Information security

Professional Memberships

  • THE INSTITUTE OF ELECTRONICS, INFORMATION AND COMMUNICATION ENGINEERS

      More details

  • IEEE Institute of Electrical and Electronics Engineers

      More details

Papers

  • A Lightweight Abnormality Detection Mechanism by Stray Packets Analysis.

    Yong Jin, Satoshi Matsuura, Takao Kondo, Tatsumi Hosokawa, Masahiko Tomoishi

    Proceedings of the 2023 ACM SIGUCCS Annual Conference(SIGUCCS)   9 - 11   2023

     More details

    Publishing type:Research paper (international conference proceedings)   Publisher:ACM  

    DOI: 10.1145/3539811.3579559

    researchmap

    Other Link: https://dblp.uni-trier.de/db/conf/siguccs/siguccs2023.html#JinMKHT23

  • Anomaly Detection on User Terminals Based on Outbound Traffic Filtering by DNS Query Monitoring and Application Program Identification

    Yong Jin, Masahiko Tomoishi, Nariyoshi Yamai

    ACM International Conference Proceeding Series   47 - 56   2021.5

     More details

    Language:English   Publishing type:Research paper (international conference proceedings)   Publisher:Association for Computing Machinery  

    Malware attacks have become one of the most critical issues in the Internet nowadays. Most types of malware, after infecting a computer, attempt contacts to the Command and Control (C&amp
    C) servers using IP addresses or Fully Qualified Domain Name (FQDN) for further instructions. In the former case, the malware connects to the C&amp
    C servers directly without DNS name resolutions, while in the later case, DNS name resolutions for obtaining the IP addresses of the C&amp
    C servers are required. In both cases, the outbound traffic will be initialized by an unrecognized application program, the malware. In this research, we focus on these peculiarities and propose an anomaly detection system on user terminals based on outbound traffic filtering by using Software Defined Network (SDN) and DNS Response Policy Zone (DNS RPZ) technologies. In the proposed system, the outbound traffic initialized by unrecognized application programs or destined to the IP addresses obtained without DNS name resolutions will be detected and blocked on user terminals. What's more, in order to reduce false positive detections, an alert message will make the users decide whether or not to allow the detected traffic. We implemented a prototype system on MacOS machine and conducted feature evaluations. According to the evaluation results, we confirmed that the proposed system worked exactly as we designed with the features of detection, blocking and alerting anomalies on user terminals.

    DOI: 10.1145/3478472.3478481

    Scopus

    researchmap

  • A Detour Strategy for Visiting Phishing URLs Based on Dynamic DNS Response Policy Zone

    Yong Jin, Masahiko Tomoishi, Nariyoshi Yamai

    2020 International Symposium on Networks, Computers and Communications, ISNCC 2020   2020.10

     More details

    Language:English   Publishing type:Research paper (international conference proceedings)   Publisher:Institute of Electrical and Electronics Engineers Inc.  

    Email based Uniform Resource Locator (URL) distribution is one of the popular ways for starting phishing attacks. Conventional anti-phishing solutions rely on security facilities and investigate all incoming emails. This makes the security facilities get overloaded and cause consequences of upgrades or new deployments even with no better options. This paper presents a novel detour strategy for the traffic of visiting potential phishing URLs based on dynamic Domain Name System (DNS) Response Policy Zone (RPZ) in order to mitigate the overloads on security facilities. In the strategy, the URLs included in the incoming emails will be extracted and the corresponding Fully Qualified Domain Name (FQDN) will be registered in the RPZ of the local DNS cache server with mapping the IP address of a special Hypertext Transfer Protocol (HTTP) proxy. The contribution of the approach is to avoid heavy investigations on all incoming emails and mitigate the overloads on security facilities by directing the traffic to phishing URLs to the special HTTP proxy connected with a set of security facilities conducting various inspections. The evaluation results on the prototype system showed that the URL extraction and FQDN registration were finished before the emails had been delivered and accesses to the URLs were successfully directed to the special HTTP proxy. The results of overhead measurements also confirmed that the proposed strategy only affected the internal email server with 11% of performance decrease on the prototype system.

    DOI: 10.1109/ISNCC49221.2020.9297211

    Scopus

    researchmap

  • A study of classification of texts into categories of cybersecurity incident and attack with topic models Reviewed

    Masahiro Ishii, Satoshi Matsuura, Kento Mori, Masahiko Tomoishi, Yong Jin, Yoshiaki Kitaguchi

    ICISSP 2020 - Proceedings of the 6th International Conference on Information Systems Security and Privacy   639 - 646   2020

     More details

    Publishing type:Research paper (international conference proceedings)  

    © Copyright 2020 by SCITEPRESS - Science and Technology Publications, Lda. All rights reserved. To improve and automate cybersecurity incident handling in security operations centers (SOCs) and computer emergency response teams (CERTs), security intelligences extracted from various internal and external sources, including incident response playbooks, incident reports in each SOCs and CERTs, the National Vulnerability Database, and social media, must be utilized. In this paper, we apply various topic models to classify text related to cybersecurity intelligence and incidents according to topics derived from incidents and cyber attacks. We analyze cybersecurity incident reports and related text in our CERT and security blog posts using naive latent Dirichlet allocation (LDA), seeded LDA, and labeled LDA topic models. Labeling text based on designated categories is difficult and time-consuming. Training the seeded model does not require text to be labeled; instead, seed words are given to allow the model to infer topic-word and document-topic distributions for the text. We show that a seeded topic model can be used to extract and classify intelligence in our CERT, and we infer text more precisely compared with a supervised topic model.

    Scopus

    researchmap

  • A Study of Classification of Texts into Categories of Cybersecurity Incident and Attack with Topic Models. Reviewed

    Masahiro Ishii 0002, Satoshi Matsuura, Kento Mori, Masahiko Tomoishi, Yong Jin, Yoshiaki Kitaguchi

    Proceedings of the 6th International Conference on Information Systems Security and Privacy(ICISSP)   639 - 646   2020

     More details

    Publishing type:Research paper (international conference proceedings)   Publisher:SCITEPRESS  

    DOI: 10.5220/0009099606390646

    researchmap

  • Detection of Hijacked Authoritative DNS Servers by Name Resolution Traffic Classification Reviewed

    Yong Jin, Masahiko Tomoishi, Satoshi Matsuura

    Proceedings - 2019 IEEE International Conference on Big Data, Big Data 2019   6084 - 6085   2019.12

     More details

    Publishing type:Research paper (international conference proceedings)  

    © 2019 IEEE. Authoritative DNS server hijacking has been a critical threat which can be hardly prevented by DNSSEC. In this work, we propose a machine learning based detection method against DNS responses replied from hijacked external authoritative DNS servers by DNS traffic data classification and heuristic analysis. The proposed method consists of header, answer, authority and additional section analysis each of which is combined with the corresponding question section. The decision maker decides if a DNS query-response pair has been related to a hijacked external authoritative DNS server by conducting heuristic analysis on the classified DNS traffic data with comparing with old cached DNS data. We have setup a local experimental network and achieved DNS traffic data (A records) of the top 500 FQDNs listed on Alexa web site for about one month and confirmed that the required features can be attracted from the DNS traffic data. Accordingly, we confirmed that it was expectable to conduct the DNS traffic classification and heuristic analysis in order to detect DNS responses replied from hijacked external authoritative DNS servers. The future work includes the DNS traffic data training and the evaluations on a local experimental network as well as in a large scale real network environment.

    DOI: 10.1109/BigData47090.2019.9006365

    Scopus

    researchmap

  • A Detection Method Against DNS Cache Poisoning Attacks Using Machine Learning Techniques: Work in Progress Reviewed

    Yong Jin, Masahiko Tomoishi, Satoshi Matsuura

    2019 IEEE 18th International Symposium on Network Computing and Applications, NCA 2019   2019.9

     More details

    Publishing type:Research paper (international conference proceedings)  

    © 2019 IEEE. DNS based domain name resolution has been known as one of the most fundamental Internet services. In the meanwhile, DNS cache poisoning attacks also have become a critical threat in the cyber world. In addition to Kaminsky attacks, the falsified data from the compromised authoritative DNS servers also have become the threats nowadays. Several solutions have been proposed in order to prevent DNS cache poisoning attacks in the literature for the former case such as DNSSEC (DNS Security Extensions), however no effective solutions have been proposed for the later case. Moreover, due to the performance issue and significant workload increase on DNS cache servers, DNSSEC has not been deployed widely yet. In this work, we propose an advanced detection method against DNS cache poisoning attacks using machine learning techniques. In the proposed method, in addition to the basic 5-tuple information of a DNS packet, we intend to add a lot of special features extracted based on the standard DNS protocols as well as the heuristic aspects such as 'time related features', 'GeoIP related features' and 'trigger of cached DNS data', etc., in order to identify the DNS response packets used for cache poisoning attacks especially those from compromised authoritative DNS servers. In this paper, as a work in progress, we describe the basic idea and concept of our proposed method as well as the intended network topology of the experimental environment while the prototype implementation, training data preparation and model creation as well as the evaluations will belong to the future work.

    DOI: 10.1109/NCA.2019.8935025

    Scopus

    researchmap

  • Anomaly Detection by Monitoring Unintended DNS Traffic on Wireless Network Reviewed

    Yong Jin, Masahiko Tomoishi, Nariyoshi Yamai

    2019 IEEE Pacific Rim Conference on Communications, Computers and Signal Processing, PACRIM 2019 - Proceedings   2019.8

     More details

    Publishing type:Research paper (international conference proceedings)  

    © 2019 IEEE. Cybersecurity threats from malware attacks has become one of the most serious issues in the Internet nowadays. Most types of malware, after intruding an individual computer, attempt to connect the corresponding Command and Control (CC) servers using IP addresses or Fully Qualified Domain Name (FQDN) and receive further instructions (e.g. attacking target IP addresses and FQDNs) from them in order to conduct subsequent cyber attacks. In recent years, it has been clarified that DNS traffic has been used for communication between the malware infection computers and the CC servers. In this research, we focus on these peculiarities and propose a method for detecting malware infected computers by monitoring unintended DNS traffic on wireless networks by collaboration with DHCP (Dynamic Host Configuration Protocol) server. By deploying the proposed system on campus wireless networks, the computers within DHCP configured environment can be detected when they are infected by some types of malware and it attempts to communicate with the corresponding CC servers using DNS (Domain Name System) protocol. In this paper, we describe the detailed design of the proposed method and the future work includes prototype implementation as well as evaluations.

    DOI: 10.1109/PACRIM47961.2019.8985052

    Scopus

    researchmap

  • Encrypted QR code based optical challenge-response authentication by mobile devices for mounting concealed file system Reviewed

    Yong Jin, Masahiko Tomoishi

    Proceedings - International Computer Software and Applications Conference   2   676 - 681   2019.7

     More details

    Publishing type:Research paper (international conference proceedings)  

    © 2019 IEEE Nowadays mobile devices have become the majority terminals used by people for social activities so that carrying business data and private information in them have become normal. Accordingly, the risk of data related cyber attacks has become one of the most critical security concerns. The main purpose of this work is to mitigate the risk of data breaches and damages caused by malware and the lost of mobile devices. In this paper, we propose an encrypted QR code based optical challenge-response authentication by mobile devices for mounting concealed file systems. The concealed file system is basically invisible to the users unless being successfully mounted. The proposed authentication scheme practically applies cryptography and QR code technologies to challenge-response scheme in order to secure the concealed file system. The key contribution of this work is to clarify a possibility of a mounting authentication scheme involving two mobile devices using a special optical communication way (QR code exchanges) which can be realizable without involving any network accesses. We implemented a prototype system and based on the preliminary feature evaluations results we confirmed that encrypted QR code based optical challenge-response is possible between a laptop and a smart phone and it can be applied to authentication for mounting concealed file systems.

    DOI: 10.1109/COMPSAC.2019.10286

    Scopus

    researchmap

  • A Lightweight and Secure IoT Remote Monitoring Mechanism Using DNS with Privacy Preservation Reviewed

    Yong Jin, Kenji Fujikawa, Masahiko Tomoishi, Ved P. Kafle

    2019 16TH IEEE ANNUAL CONSUMER COMMUNICATIONS & NETWORKING CONFERENCE (CCNC)   2019

     More details

    Language:English   Publishing type:Research paper (international conference proceedings)   Publisher:IEEE  

    IoT remote control is faced with scalability, secure communication and privacy preservation issues and conventional solutions (HTTPS) have disclosed poor scaling problem and privacy concerns. In this paper, we propose a novel lightweight and secure IoT remote monitoring mechanism using DNS with privacy preservation. Basically, the communication between IoT devices and gateways uses the conventional protocols as usual such as CoAP and MQTT while only the remote monitoring uses DNS protocol. That is, encrypted IoT data, after being encoded with base64, is stored as a DNS TXT record of the domain name of the IoT device and only the designated users are allowed to query and decrypt the data based on TSIG authentication of DNS protocol and asymmetric cryptography. We implemented a prototype system over name-bound virtual networks (NBVNs) in which all virtual nodes are registered in DNS automatically and the network traffic is restricted within each NBVN. Through the preliminary evaluations we confirmed the effectiveness of secure communication and privacy preservation in IoT remote monitoring in the proposed mechanism.

    Web of Science

    researchmap

  • A Secure End-to-End Key Exchange Mechanism by Cooperation of Multiple Devices Using QR Codes. Reviewed

    Yong Jin, Masahiko Tomoishi

    29th International Telecommunication Networks and Applications Conference(ITNAC)   1 - 7   2019

     More details

    Publishing type:Research paper (international conference proceedings)   Publisher:IEEE  

    DOI: 10.1109/ITNAC46935.2019.9078020

    researchmap

  • Detection of Hijacked Authoritative DNS Servers by Name Resolution Traffic Classification. Reviewed

    Yong Jin, Masahiko Tomoishi, Satoshi Matsuura

    2019 IEEE International Conference on Big Data (IEEE BigData)   6084 - 6085   2019

     More details

    Publishing type:Research paper (international conference proceedings)   Publisher:IEEE  

    DOI: 10.1109/BigData47090.2019.9006365

    researchmap

  • A secure in-depth file system concealed by GPS-based mounting authentication for mobile devices Reviewed

    Yong Jin, Masahiko Tomoishi, Satoshi Matsuura, Yoshiaki Kitaguchi

    IEICE Transactions on Information and Systems   E101D ( 11 )   2612 - 2621   2018.11

     More details

    Publishing type:Research paper (scientific journal)  

    © 2018 The Institute of Electronics, Information and Communication Engineers. Data breach and data destruction attack have become the critical security threats for the ICT (Information and Communication Technology) infrastructure. Both the Internet service providers and users are suffering from the cyber threats especially those to confidential data and private information. The requirements of human social activities make people move carrying confidential data and data breach always happens during the transportation. The Internet connectivity and cryptographic technology have made the usage of confidential data much secure. However, even with the high deployment rate of the Internet infrastructure, the concerns for lack of the Internet connectivity make people carry data with their mobile devices. In this paper, we describe the main patterns of data breach occur on mobile devices and propose a secure in-depth file system concealed by GPS-based mounting authentication to mitigate data breach on mobile devices. In the proposed in-depth file system, data can be stored based on the level of credential with corresponding authentication policy and the mounting operation will be only successful on designated locations. We implemented a prototype system using Veracrypt and Perl language and confirmed that the in-depth file system worked exactly as we expected by evaluations on two locations. The contribution of this paper includes the clarification that GPS-based mounting authentication for a file system can reduce the risk of data breach for mobile devices and a realization of prototype system.

    DOI: 10.1587/transinf.2017ICP0017

    Web of Science

    Scopus

    researchmap

  • A Secure In-Depth File System Concealed by GPS-Based Mounting Authentication for Mobile Devices Reviewed

    Yong Jin, Masahiko Tomoishi, Satoshi Matsuura, Yoshiaki Kitaguchi

    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS   E101D ( 11 )   2612 - 2621   2018.11

     More details

    Language:English   Publishing type:Research paper (scientific journal)   Publisher:IEICE-INST ELECTRONICS INFORMATION COMMUNICATIONS ENG  

    Data breach and data destruction attack have become the critical security threats for the ICT (Information and Communication Technology) infrastructure. Both the Internet service providers and users are suffering from the cyber threats especially those to confidential data and private information. The requirements of human social activities make people move carrying confidential data and data breach always happens during the transportation. The Internet connectivity and cryptographic technology have made the usage of confidential data much secure. However, even with the high deployment rate of the Internet infrastructure, the concerns for lack of the Internet connectivity make people carry data with their mobile devices. In this paper, we describe the main patterns of data breach occur on mobile devices and propose a secure in-depth file system concealed by GPS-based mounting authentication to mitigate data breach on mobile devices. In the proposed in-depth file system, data can be stored based on the level of credential with corresponding authentication policy and the mounting operation will be only successful on designated locations. We implemented a prototype system using Veracrypt and Perl language and confirmed that the in-depth file system worked exactly as we expected by evaluations on two locations. The contribution of this paper includes the clarification that GPS-based mounting authentication for a file system can reduce the risk of data breach for mobile devices and a realization of prototype system.

    DOI: 10.1587/transinf.2017ICP0017

    Web of Science

    researchmap

  • A Client Based DNSSEC Validation Mechanism with Recursive DNS Server Separation Reviewed

    Yong Jin, Masahiko Tomoishi, Nariyoshi Yamai

    2018 INTERNATIONAL CONFERENCE ON INFORMATION AND COMMUNICATION TECHNOLOGY CONVERGENCE (ICTC)   148 - 153   2018

     More details

    Language:English   Publishing type:Research paper (international conference proceedings)   Publisher:IEEE  

    DNSSEC has been proposed to provide data origin authentication and data integrity between recursive DNS server and authoritative zone server. Although DNSSEC is an effective countermeasure to DNS cache poisoning attack, it still has low deployment rate in the Internet due to the significant workload increase on recursive DNS servers. Moreover, current DNSSEC operation does not cover end clients and the recursive DNS server separation has not been considered so that end users do not intend to use free and powerful public recursive DNS servers due to security concerns. In this paper, we propose a client based DNSSEC validation mechanism with recursive DNS server separation based on query types. DNSSEC related record types such as RRSIG, DNSKEY, DS, etc. will be forwarded to a trusted internal recursive DNS server while normal record types such as A, AAAA, MX, etc. will be forwarded to public recursive DNS server, and eventually, DNSSEC validation will be performed on end clients. Consequently, not only end clients can obtain the benefit of DNSSEC but also the workload increase of internal recursive DNS servers can be mitigated. We implemented a prototype system and evaluated the features on a local experimental network. Based on the results, we confirmed that the prototype system worked effectively and it is possible to prevent end clients from DNS cache poisoning attacks by the proposed mechanism.

    Web of Science

    researchmap

  • A Client based Anomaly Traffic Detection and Blocking Mechanism by Monitoring DNS Name Resolution With User Alerting Feature Reviewed

    Yong Jin, Kunitaka Kakoi, Nariyoshi Yamai, Naoya Kitagawa, Masahiko Tomoishi

    2018 INTERNATIONAL CONFERENCE ON CYBERWORLDS (CW)   351 - 356   2018

     More details

    Language:English   Publishing type:Research paper (international conference proceedings)   Publisher:IEEE  

    Malware has become one of the most critical targets of network security solutions nowadays. Many types of malware receive further instructions from the C&C servers and the attack targets may be instructed by IP addresses which causes direct attacks without DNS name resolution from the malware-infected computers. In the meanwhile, several programs that are hidden from the users (e.g. malware, virus, etc.) may perform DNS name resolutions for cyber attacks or other communications. In this paper, we propose a client based anomaly traffic detection and blocking mechanism by monitoring DNS name resolution per application program. In the proposed mechanism, by the collaboration of DNS proxy and packet filter, DNS traffic is monitored on the client and the traffic destined to the IP addresses obtained without DNS name resolution or the traffic from unrecognized programs will be detected and blocked. In addition, in order to mitigate false positive detection, an alert-window will be shown to let the users decide whether to allow the traffic or not. We implemented a prototype system on a Windows 7 client and confirmed that the proposed mechanism worked as expected.

    DOI: 10.1109/CW.2018.00070

    Web of Science

    researchmap

  • A Client Based DNSSEC Validation System with Adaptive Alert Mechanism Considering Minimal Client Timeout Reviewed

    Yong Jin, Kunitaka Kakoi, Nariyoshi Yamai, Naoya Kitagawa, Masahiko Tomoishi

    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS   E100D ( 8 )   1751 - 1761   2017.8

     More details

    Language:English   Publishing type:Research paper (scientific journal)   Publisher:IEICE-INST ELECTRONICS INFORMATION COMMUNICATIONS ENG  

    The widespread usage of computers and communication networks affects people's social activities effectively in terms of intercommunication and the communication generally begins with domain name resolutions which are mainly provided by DNS (Domain Name System). Meanwhile, continuous cyber threats to DNS such as cache poisoning also affects computer networks critically. DNSSEC (DNS Security Extensions) is designed to provide secure name resolution between authoritative zone servers and DNS full resolvers. However high workload of DNSSEC validation on DNS full resolvers and complex key management on authoritative zone servers hinder its wide deployment. Moreover, querying clients use the name resolution results validated on DNS full resolvers, therefore they only get errors when DNSSEC validation fails or times out. In addition, name resolution failure can occur on querying clients due to technical and operational issues of DNSSEC. In this paper, we propose a client based DNSSEC validation system with adaptive alert mechanism considering minimal querying client timeout. The proposed system notifies the user of alert messages with answers even when the DNSSEC validation on the client fails or timeout so that the user can determine how to handle the received answers. We also implemented a prototype system and evaluated the features on a local experimental network as well as in the Internet. The contribution of this article is that the proposed system not only can mitigate the workload of DNS full resolvers but also can cover querying clients with secure name resolution, and by solving the existing operation issues in DNSSEC, it also can promote DNSSEC deployment.

    DOI: 10.1587/transinf.2016ICP0028

    Web of Science

    researchmap

  • A Client Based DNSSEC Validation System with Adaptive Alert Mechanism Considering Minimal Client Timeout Reviewed

    JIN Yong, KAKOI Kunitaka, YAMAI Nariyoshi, KITAGAWA Naoya, TOMOISHI Masahiko

    IEICE Transactions on Information and Systems   100 ( 8 )   1751 - 1761   2017

     More details

    Language:English   Publisher:The Institute of Electronics, Information and Communication Engineers  

    <p>The widespread usage of computers and communication networks affects people's social activities effectively in terms of intercommunication and the communication generally begins with domain name resolutions which are mainly provided by DNS (Domain Name System). Meanwhile, continuous cyber threats to DNS such as cache poisoning also affects computer networks critically. DNSSEC (DNS Security Extensions) is designed to provide secure name resolution between authoritative zone servers and DNS full resolvers. However high workload of DNSSEC validation on DNS full resolvers and complex key management on authoritative zone servers hinder its wide deployment. Moreover, querying clients use the name resolution results validated on DNS full resolvers, therefore they only get errors when DNSSEC validation fails or times out. In addition, name resolution failure can occur on querying clients due to technical and operational issues of DNSSEC. In this paper, we propose a client based DNSSEC validation system with adaptive alert mechanism considering minimal querying client timeout. The proposed system notifies the user of alert messages with answers even when the DNSSEC validation on the client fails or timeout so that the user can determine how to handle the received answers. We also implemented a prototype system and evaluated the features on a local experimental network as well as in the Internet. The contribution of this article is that the proposed system not only can mitigate the workload of DNS full resolvers but also can cover querying clients with secure name resolution, and by solving the existing operation issues in DNSSEC, it also can promote DNSSEC deployment.</p>

    DOI: 10.1587/transinf.2016ICP0028

    researchmap

  • Design and Implementation of A Client Based DNSSEC Validation and Alert System Reviewed

    Kunitaka Kakoi, Yong Jin, Nariyoshi Yamai, Naoya Kitagawa, Masahiko Tomoishi

    PROCEEDINGS 2016 IEEE 40TH ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE WORKSHOPS (COMPSAC), VOL 2   8 - 13   2016

     More details

    Language:English   Publishing type:Research paper (international conference proceedings)   Publisher:IEEE  

    The widespread computers in all over the world are connected with each other via the Internet and their communications normally begin with domain name resolutions which are mainly provided by DNS (Domain Name System). Recent cyber threats to DNS system attract much attentions of DNSSEC (DNS Security Extensions) which can provide secure name resolution services. However the high workload on DNS full resolvers and complex key management hinders its wide deployment. In addition, in the current DNSSEC protocol, secure name resolution does not cover end clients. In order to solve the problem, in this paper, we propose a client based DNSSEC validation and alert system. The proposed system not only can mitigate the workload of DNS full resolvers but also can perform DNSSEC validation on clients. Furthermore, the system also notifies the user of failure message so that the user can determine whether trust the answer or not rather than just receives "server failure" error in case DNSSEC validation fails. We also implemented a prototype system and evaluated the proposed features on a local experimental network. Based on the evaluation results, we confirmed that the proposed system worked well as we expected.

    DOI: 10.1109/COMPSAC.2016.91

    Web of Science

    researchmap

  • Report on FME 2001 : Formal Methods for increasing Software Productivity.

    TOMOISHI Masahiko, Masahiko Tomoishi, Department of Computer, Science Graduate School of Information Science, Engineering Tokyo, Institute of Technology

    Computer Software   18 ( 4 )   455 - 460   2001.7

     More details

    Language:Japanese   Publisher:日本ソフトウェア科学会  

    DOI: 10.11309/jssst.18.455

    CiNii Books

    researchmap

  • Unification-based resolution method for modal logic with finite frames

    Shigeki Hagihara, Masahiko Tomoishi, Naoki Yonezaki

    Computer Software   18 ( 0 )   78 - 91   2000.12

     More details

    Language:Japanese   Publisher:日本ソフトウェア科学会  

    システムが停止することを仮定した性質(例えば,「システムの終了は必ず正常終了である」という性質)を時間論理を用いて検証する場合には,有限な時間構造を意味論に持つ様相論理KWを用いることができる。本論文では,KWに対する様相演算子の列の統一化を用いる分解証明法を提案する。式が有限な時間構造のモデルを持たないことを確認するためには,もし式がモデルを持つならば,無限に遷移するモデルしか持たないことを調べる必要がある。ところが,様相演算子列の統一化を用いる証明法で,それを確認することは困難であった。本論文では,有限な時間構造と式の充足可能性が一致する非反復構造を導入した。式が非反復構造のモデルを持たないことを確認するためには,もし式がモデルを持つならば,繰り返し同じ遷移をするモデルしか持たないことを調べればよい。この性質に基づき,KWで式が充足不能であることを調べる証明法を構成した

    Scopus

    researchmap

  • 有限フレームを意味的基礎として持つ様相論理に対する分解証明法

    萩原茂樹, 友石正彦, 米崎直樹

    コンピュータソフトウェア   18 ( 0 )   78 - 91   2000

  • Classfication of Reactive System Specifications in Temporal Logic

    MORI Ryosei, TOMOISHI Masahiko, YONEZAKI Naoki, Ryosei Mori, Masahiko Tomoishi, Naoki Yonezaki, Department of Comuter, Science Tokyo, Insutitute of Technology, Department of Comuter, Science Tokyo, Insutitute of Technology, Department of Comuter, Science Tokyo, Insutitute of Technology

    コンピュータソフトウェア = Computer software   15 ( 3 )   213 - 225   1998.5

     More details

    Language:Japanese   Publisher:日本ソフトウェア科学会  

    CiNii Books

    researchmap

▼display all

MISC

  • Prototype of Monitoring System for Remote Home Healthcare Using DNS

    陸子健, 金勇, 山井成良, 友石正彦

    情報処理学会研究報告(Web)   2021 ( IOT-52 )   2021

  • 東工大CERTにおけるインシデント対応の分析とその自動化に関する考察

    石井将大, 森健人, 松浦知史, 金勇, 北口善明, 友石正彦

    情報処理学会研究報告(Web)   2018 ( IOT-43 )   Vol.2018‐IOT‐43,No.2,1‐8 (WEB ONLY)   2018.9

     More details

    Language:Japanese  

    J-GLOBAL

    researchmap

  • Suspicious Access Detection and Blocking System on User Terminals for Outbound Measure Based on DNS Queries

    栫邦雄, 栫邦雄, 山井成良, JIN Yong, 北川直哉, 友石正彦

    情報処理学会研究報告(Web)   2018 ( IOT-42 )   Vol.2018‐IOT‐42,No.9,1‐6 (WEB ONLY)   2018.6

     More details

    Language:Japanese  

    J-GLOBAL

    researchmap

  • A Secure Container-based Backup Mechanism to Survive Destructive Ransomware Attacks

    Yong Jin, Masahiko Tomoishi, Satoshi Matsuura, Yoshiaki Kitaguchi

    2018 International Conference on Computing, Networking and Communications, ICNC 2018   1 - 6   2018.6

     More details

    © 2018 IEEE. The threats of destructive ransomware keep increasing and current security facilities (firewall, IDS/IPS, etc.) and backup systems cannot effectively protect data from the attacks in real time. In this paper, we propose a secure container-based backup mechanism to survive destructive ransomware attacks. In the mechanism, the backup process takes place in a highly restricted local docker container and only the container can access both source and backup data stored in the local and remote storages. That is, the host is only allowed to access the source data and the container is only allowed to perform backup process without any other communications. Consequently, any other processes in the host cannot access the backup data stored in the container and the remote storage. Thus even if the host and the container are completely destroyed, the data can be recovered from the remote storage. We implemented a prototype system and confirmed that it can backup data with high usability and store the backup data securely.

    DOI: 10.1109/ICCNC.2018.8390376

    Scopus

    researchmap

  • Web server access trend analysis based on the Poisson distribution

    Shigeki Hagihara, Yoshiharu Fushihara, Masaya Shimakawa, Masahiko Tomoishi, Naoki Yonezaki

    ACM International Conference Proceeding Series   256 - 261   2017.2

     More details

    Language:English   Publisher:Association for Computing Machinery  

    To determine the amount of computational resources such as CPU power, memory, and network bandwidth to be assigned to web servers, it is useful to capture daily access data. These can be captured in advance from access logs. Moreover, to determine thresholds for detecting attacks such as distributed denial of service, where the rate of access varies significantly, it is important to know usual access trends for a given server. In this paper, we propose a method for capturing patterns of access to web servers by analyzing access logs. Instead of directly analyzing the periodicity of access using Fourier transforms, we analyze access trends based on an abstract model where only changes to access frequency are captured. This abstract model, constructed by determining whether access frequency follows a Poisson distribution, is simpler than the original access log and is specialized as it only contains information about access frequency changes. Therefore, it is easy to capture access trends based on this model. We analyzed two access logs using our method, the logs of the web servers at Saskatchewan University and those of the National Aeronautics and Space Administration. We confirmed that our method can be used to capture several characteristic access trends.

    DOI: 10.1145/3056662.3056701

    Scopus

    researchmap

  • Cache Function Activation on Multi-process DNSSEC Validation System by Multi-threading

    中村将也, 栫邦雄, JIN Yong, 山井成良, 北川直哉, 友石正彦

    電子情報通信学会技術研究報告   116 ( 491(IA2016 90-114) )   97‐102   2017.2

     More details

    Language:Japanese  

    J-GLOBAL

    researchmap

  • A Secure and Lightweight IoT Device Remote Monitoring and Control Mechanism Using DNS Reviewed

    Yong Jin, Masahiko Tomoishi, Nariyoshi Yamai

    2017 IEEE 41ST ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), VOL 2   282 - 283   2017

     More details

    Language:English   Publisher:IEEE  

    Many reports predicted that the number of connected IoT (Internet of Things) devices will reach to billions in the next several years, accordingly, how to securely and effectively manage, monitor and control them becomes a critical problem. In conventional IoT solutions, direct SSL/TLS based HTTP connections to IoT devices with high overhead are required and encryption is not considered due to low computing capability and memory capacity of IoT devices. In this paper, we propose an integrated mechanism using DNS (Domain Name System) to accomplish the objective. In the proposed mechanism, names or IDs of IoT devices are managed by DNS server and the monitoring and control are conducted by the collaboration of DNS name resolution, DNS dynamic update and DNS zone transfer. Considering the security and privacy protection, the status and control command for IoT devices described in the corresponding DNS TXT records will be encrypted and TSIG (Transaction SIGnatures) will be used for authentication to restrict the clients allowed to monitor and control the IoT devices.

    DOI: 10.1109/COMPSAC.2017.33

    Web of Science

    researchmap

  • Cache Function Activation on A Client Based DNSSEC Validation and Alert System by Multithreading Reviewed

    Kunitaka Kakoi, Yong Jin, Nariyoshi Yamai, Naoya Kitagawa, Masahiko Tomoishi

    2017 IEEE 41ST ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), VOL 2   37 - 42   2017

     More details

    Language:English   Publisher:IEEE  

    Domain Name System (DNS) is one of the most important services of the Internet since most communications normally begin with domain name resolutions provided by DNS. However, DNS has vulnerability against some kind of attacks such as DNS spoofing, DNS cache poisoning, and so on. DNSSEC is an security extension of DNS to provide secure name resolution services by using digital signature based on public key cryptography. However, there are several problems with DNSSEC such as failing resolution in case of validation failure, increasing the load of DNS full resolver, and so on. To mitigate these problems, we proposed a Client Based DNSSEC Validation System. This system performs DNSSEC validation on the client, and in case of validation failure, it forwards the failed response and alerts the user to the fact. However, this system has a problem that it inactivates the cache function of validation library so that it always performs DNSSEC validation even for the same query. In this paper, we report how to solve this problem by multithreading of DNSSEC validation system.

    DOI: 10.1109/COMPSAC.2017.78

    Web of Science

    researchmap

  • Efficient Detection of Suspicious DNS Traffic by Resolver Separation per Application Program Reviewed

    Yong Jin, Kunitaka Kakoi, Masahiko Tomoishi, Nariyoshi Yamai

    2017 INTERNATIONAL CONFERENCE ON INFORMATION AND COMMUNICATION TECHNOLOGY CONVERGENCE (ICTC)   87 - 92   2017

     More details

    Language:English   Publisher:IEEE  

    With the development of ICT (Information and Communication Technology), computer and the Internet have become indispensable for people's social activities while cyber security threats keep on increase trend. Unfortunately, the current popular security facilities cannot efficiently detect cyber attacks due to a tremendous amount of network traffic needs to be analyzed. In this paper, we focus on DNS (Domain Name System) name resolution and propose an efficient detection method of suspicious DNS traffic by resolver separation per application program. Based on that almost all kinds of software including malware use DNS name resolution, in the proposed method, the DNS queries will be forwarded to different DNS full resolver per application program. The DNS queries from well-known application programs such as Internet browsers and anti-virus software will be forwarded to a normal DNS full resolver while others from unknown application programs such as malware will be forwarded to a highly-monitored DNS full resolver. Consequently, the DNS queries from unknown application programs can be detected immediately since there will be only little DNS traffic need to be analyzed compare to the whole network traffic. We implemented a prototype system on a windows operating system and evaluated the features on a local experimental network. According to the evaluation results, we confirmed that the proposed method can precisely forward the DNS queries based on the application programs correctly, and also the DNS queries are logged on the client by mapping with the corresponding application program which initialized the DNS queries.

    DOI: 10.1109/ICTC.2017.8190948

    Web of Science

    researchmap

  • Combining Unification and Rewriting in Proofs for Modal Logics with First-order Undefinable Frames Reviewed

    Shigeki Hagihara, Masahiko Tomoishi, Masaya Shimakawa, Naoki Yonezaki

    PROCEEDINGS OF THE 2017 5TH INTERNATIONAL CONFERENCE ON MACHINERY, MATERIALS AND COMPUTING TECHNOLOGY (ICMMCT 2017)   126   676 - 683   2017

     More details

    Language:English   Publisher:ATLANTIS PRESS  

    We provide a unification-based resolution method for basic modal logics. Because we use a clausal normal form that is quite similar to that in first-order logic, our method has good prospects for importing proof strategies for resolution methods from first-order logic. Furthermore, we show a solution for obtaining a resolution method for the modal logic KM, the frames of which are first-order and undefinable. It is impossible to make a unification rule for the modal logics of first-order undefinable frames in a similar way to that of basic modal logics. In this paper, we use a clausal rewriting rule for KM in addition to modal unification. We expect that this kind of adaptation can be applied to the construction of unification-based proof methods for other modal logics with first-order undefinable frames.

    Web of Science

    researchmap

  • An In-Depth Concealed File System with GPS Authentication Adaptable for Multiple Locations Reviewed

    Yong Jin, Masahiko Tomoishi, Satoshi Matsuura

    2017 IEEE 41ST ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), VOL 1   608 - 613   2017

     More details

    Language:English   Publisher:IEEE  

    Security threats from cyber attacks never stop threatening human's social activities. Even though, carrying mobile devices with confidential data is still popular among people without constraint due to business needs and usability. In this paper, we propose an in-depth concealed file system with GPS authentication adaptable for multiple locations in order to mitigate data breaches and file destructions on mobile devices. The proposed file system has in-depth layout and is mountable only when the mobile device is in the designated areas using GPS authentication. Different security policies can be set for each layer and data can be separately stored in each layer based on the confidentiality. Moreover, usability is considered as high priority and an automatic mounting feature is also introduced since people cannot be bordered to run the program a lot times. We implemented a 2-layer prototype system with combination of GPS only authentication (lightweight) and collaborated authentication (mobile device and smart phone). According to the preliminary evaluation results, we confirmed that the proposed in-depth concealed file system can contribute to mitigate the risk of data breaches and destructions on mobile devices.

    DOI: 10.1109/COMPSAC.2017.56

    Web of Science

    researchmap

  • オンプレミスで実現する業務効率化のためのOSS基盤環境構築

    森健人, 松浦知史, 金勇, 友石正彦

    情報処理学会研究報告(Web)   2016 ( SPT-20 )   Vol.2016‐SPT‐20,No.10,1‐8 (WEB ONLY)   2016.9

     More details

    Language:Japanese  

    J-GLOBAL

    researchmap

  • Design and Implementation of A Client Based DNSSEC Validation and Alert System Reviewed

    栫邦雄, JIN Yong, 山井成良, 北川直哉, 友石正彦

    電子情報通信学会技術研究報告   116 ( 65(ICM2016 1-7) )   13‐20 - 13   2016.5

     More details

  • 拡張性を考慮した小規模仮想化基盤の構築 (技術と社会・倫理)

    松浦 知史, 森 健人, 金 勇, 友石 正彦

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報   115 ( 481 )   165 - 172   2016.3

     More details

    Language:Japanese   Publisher:電子情報通信学会  

    researchmap

  • 拡張性を考慮した小規模仮想化基盤の構築 (インターネットアーキテクチャ)

    松浦 知史, 森 健人, 金 勇, 友石 正彦

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報   115 ( 482 )   165 - 172   2016.3

     More details

    Language:Japanese   Publisher:電子情報通信学会  

    researchmap

  • 拡張性を考慮した小規模仮想化基盤の構築

    松浦知史, 森健人, 金勇, 友石正彦

    情報処理学会研究報告(Web)   2016 ( IOT-32 )   2016-IOT-32(27) (WEB ONLY)   2016.2

     More details

    Language:Japanese  

    J-GLOBAL

    researchmap

  • Enhancement of VPN authentication Using GPS Information with Geo-privacy Protection Reviewed

    Yong Jin, Masahiko Tomoishi, Satoshi Matsuura

    2016 25TH INTERNATIONAL CONFERENCE ON COMPUTER COMMUNICATIONS AND NETWORKS (ICCCN)   2016

     More details

    Language:English   Publisher:IEEE  

    VPN (Virtual Private Network) technology is well used for remote access to the internal server in order to mitigate intrusion attacks and data breaches. In the current VPN technologies, PKI (Public Key Infrastructure) based certificate authentication and user ID/Password authentication are well used. However, in case of password leakage and lost of mobile devices, those authentication methods cannot effectively prevent the malicious accesses. In this paper, we propose an enhancement method of VPN authentication using GPS (Global Positioning System) information with geo-privacy protection. In this method, the GPS information of the client is used for VPN authentication without leaking the raw GPS coordinates of the client. Specifically, the hash values of GPS coordinate ranges will be registered on the VPN authentication server in order to protect the user geo-privacy. By using the proposed method, the remote access via VPN tunnel can be controlled within all designated areas so that the risk of intrusion attacks can be mitigated significantly. We achieved the GPS coordinates in our lab for one month and checked their hit rates in the GPS coordinate ranges achieved from the Google Maps. The results showed about 99.29% and 92.96% hit rates in the latitude and longitude respectively which are acceptable for real operation.

    Web of Science

    researchmap

  • An Advanced Client Based DNSSEC Validation and Preliminary Evaluations Toward Realization Reviewed

    Yong Jin, Masahiko Tomoishi, Nariyoshi Yamai

    2016 INTERNATIONAL CONFERENCE ON INFORMATION AND COMMUNICATION TECHNOLOGY CONVERGENCE (ICTC 2016): TOWARDS SMARTER HYPER-CONNECTED WORLD   178 - 183   2016

     More details

    Language:English   Publisher:IEEE  

    DNSSEC (Domain Name System Security Extensions) is designed to provide security functions for the current DNS protocol. However, DNSSEC yet has low deployment rate in the Internet due to its heavy workload on DNS full resolvers and high administrative cost. Furthermore, DNSSEC does not cover the last one mile in name resolution: between the DNS full resolver and client. In order to provide complete DNSSEC service between authoritative zone servers and clients, a new DNSSEC validation mechanism with acceptable workload on DNS full resolver and client is required. In this paper, we propose an advanced client based DNSSEC validation mechanism and compare the DNSSEC performance between DNS full resolver and client based on evaluations in a local experimental network. By validating DNSSEC on each client, the proposed mechanism can reduce the workload of DNS full resolvers and also can provide secure name resolution for each client. According to the results of preliminary evaluations we confirmed that it is possible to reduce the workload of DNS full resolver by transferring the DNSSEC validation process to clients with acceptable extra workload. More importantly, the benefit of DNSSEC can be extended to clients with secure name resolution service.

    DOI: 10.1109/ICTC.2016.7763463

    Web of Science

    researchmap

  • Design of A Concealed File System Adapted for Mobile Devices Based on GPS Information

    Yong Jin, Masahiko Tomoishi, Satoshi Matsuura

    PROCEEDINGS 2016 IEEE 40TH ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE WORKSHOPS, VOL 1   1   459 - 464   2016

     More details

    Language:English   Publisher:IEEE COMPUTER SOC  

    The Internet Security Threat Report by Symantec announced that the number of data breaches increased 23 percent in 2014 and the causes by theft or loss of devices reached to 21 percent. Carrying mobile devices with business data and private information is indispensable for human's social activities nowadays and unexpected data breach is one of the severe ongoing issues in cyber security. In this paper, we propose a concealed file system adapted for mobile devices based on GPS (Global Positioning System) information which is only mountable in the designated area. Differs from conventional encryption technologies, the proposed file system can be completely isolated from the viruses and attacks outside the designated area. Moreover, instead of the GPS information of the designated area, the encrypted hash value will be stored in mobile devices for the privacy concerns. We statistically analyzed the GPS information logged in our lab and defined an algorithm for deciding the designated area without leaking the GPS information. Based on the algorithm, we evaluated the proposed file system using Veracrypt by adding the hash of GPS information indicating the designated area as one of the attributes for mounting authentication. As a result, we confirmed that the proposed file system was mounted with about 91% success rate within average in the designated area even with noise interference.

    DOI: 10.1109/COMPSAC.2016.93

    Web of Science

    Scopus

    researchmap

  • Web server performance enhancement by suppressing network traffic for high performance client

    Yong Jin, Masahiko Tomoishi

    2015 17TH ASIA-PACIFIC NETWORK OPERATIONS AND MANAGEMENT SYMPOSIUM APNOMS   448 - 451   2015

     More details

    Language:English   Publisher:IEEE  

    In a high performance computer network system especially that has high-speed networks, an imbalance problem occurs in terms of that network performance is significantly higher than computer capacity. The problem deteriorates performance of the entire system by ineffectively overloading application servers by few high performance clients. In this paper, we present performance analysis and validation of a web server and confirm the possibility of transparent performance enhancement for a high performance computer network system by only changing the configuration of network facilities such as switches and routers. We constructed a local experimental web system and reproduced several cases in which the problem occurred and confirmed that it is possible to solve the problem by only suppressing network traffic on the communication lines for high performance clients. By practically using the network traffic control method it is expectable to provide best performance of application systems in a high-speed network environment in the future.

    DOI: 10.1109/APNOMS.2015.7275385

    Web of Science

    Scopus

    researchmap

  • POP(Point-of-Presence) Linkage between Computer Centers as an E-Science Infrastructure

    滝澤真一朗, 松岡聡, 佐藤仁, 東田学, 友石正彦, 實本英之

    情報処理学会研究報告(CD-ROM)   2010 ( 3 )   ROMBUNNO.HPC-126,NO.31   2010.10

     More details

    Language:Japanese  

    J-GLOBAL

    researchmap

  • Resource Federation for e-science by a Point-of-Presence

    TAKIZAWA Shin'ichiro, MATSUOKA Satoshi, SATO Hitoshi, HIGASHIDA Manabu, TOMOISHI Masahiko

    IEICE technical report. Internet Architecture   110 ( 206 )   19 - 24   2010.9

     More details

    Language:Japanese   Publisher:The Institute of Electronics, Information and Communication Engineers  

    As an e-Science infrastructure, We propose a network environment where site resources are federated by a point-of-presence named RENKEI-PoP. RENKEI-PoPs are located in sites that provide resources for e-Science, are integrated with site local resources, and relay communications between sites by cooperating with each other using a grid security infrastructure. RENKEI-PoP provides 1) a virtual machine hosting environment that executes e-science infrastructure services and 2) a general-purpose data transfer/sharing environment. We installed RENKEI-PoPs in eight sites in Japan and connected them to SINET 10Gbps network. We show the current RENKEI-PoP system and its network and storage access performance.

    CiNii Books

    researchmap

  • Resource Federation for e-science by a Point-of-Presence

    滝澤真一朗, 松岡聡, 佐藤仁, 東田学, 友石正彦

    電子情報通信学会技術研究報告   110 ( 206(IA2010 29-38) )   19 - 24   2010.9

     More details

    Language:Japanese   Publisher:The Institute of Electronics, Information and Communication Engineers  

    As an e-Science infrastructure, We propose a network environment where site resources are federated by a point-of-presence named RENKEI-PoP. RENKEI-PoPs are located in sites that provide resources for e-Science, are integrated with site local resources, and relay communications between sites by cooperating with each other using a grid security infrastructure. RENKEI-PoP provides 1) a virtual machine hosting environment that executes e-science infrastructure services and 2) a general-purpose data transfer/sharing environment. We installed RENKEI-PoPs in eight sites in Japan and connected them to SINET 10Gbps network. We show the current RENKEI-PoP system and its network and storage access performance.

    CiNii Books

    J-GLOBAL

    researchmap

  • POP(Point-of-Presence) Linkage between Computer Centers as an E-Science Infrastructure

    TAKIZAWA SHIN'ICHIRO, MATSUOKA SATOSHI, SATO HITOSHI, HIGASHIDA MANABU, TOMOISHI MASAHIKO, JITSUMOTO HIDEYUKI

    研究報告ハイパフォーマンスコンピューティング(HPC)   2010 ( 31 )   1 - 8   2010.7

     More details

    Language:Japanese   Publisher:情報処理学会  

    ネットワーク分散した種々のリソースを統合して,科学技術の新発見・融合研究領域の開拓を促進する研究手法であるe-サイエンスが注目されている.e-サイエンス実現基盤として,我々は RENKEI-PoP と名付けた Point-of-Presence にて拠点間を接続するネットワーク環境を提案する.RENKEI-PoP は e-サイエンスリソースを提供する拠点に設置され,拠点内リソースとは強く結合し,RENKEI-PoP 間ではグリッド認証により連携して,拠点間通信の中継を行う.RENKEI-PoP は,1) e-サイエンス基盤システムを構成するサービス群の実行環境,および分散システム開発・評価環境を仮想マシンで実現する仮想ホスティングと,2) 拠点間の汎用データ転送・共有環境を提供する.我々は,日本国内7拠点に RENKEI-PoP を設置し,SINET の提供する 10 Gbps ネットワークで接続した.現状のシステム構成,ネットワーク,ストレージアクセスの評価結果を示す.As an e-Science infrastructure, We propose a network environment where site resources are connected by a point-of-presence named RENKEI-PoP. RENKEI-PoPs are located in sites that provide resources for e-Science, are integrated with site local resources, and relay communications between sites by cooperating with each other using a grid security infrastructure. RENKEI-PoP provides 1) a virtual hosting environment that supports running and developing e-science infrastructure services and 2)a general-purpose data transfer/sharing environment. We installed RENKEI-PoPs in seven sites in Japan and connected them to SINET 10Gbps network. We propose the current RENKEI-PoP system and show its performance of network and storage access.

    CiNii Books

    researchmap

  • Design and deployment of campus-wide network using virtual network technologies

    TOMOISHI Masahiko, MASUI Kenji, IIDA Katsuyoshi

    IEICE technical report   109 ( 437 )   207 - 212   2010.2

     More details

    Language:Japanese   Publisher:The Institute of Electronics, Information and Communication Engineers  

    In campus-wide network, reliable and the state-of-the-art technology with low operational costs must be deployed. In this paper, we describe the design and deployment of the campus-wide network Titanet3, which will be deplyed in Tokyo Tech in March 2010. Furhtermore, virtual network technology will be useful in campus-wide network, so that we introduce such technologies which will be employed in Titanet3.

    researchmap

  • Design and deployment of campus-wide network using virtual network technologies

    友石正彦, 益井賢次, 飯田勝吉

    電子情報通信学会技術研究報告   109 ( 438(IA2009 96-125) )   207 - 212   2010.2

     More details

    Language:Japanese   Publisher:The Institute of Electronics, Information and Communication Engineers  

    In campus-wide network, reliable and the state-of-the-art technology with low operational costs must be deployed. In this paper, we describe the design and deployment of the campus-wide network Titanet3, which will be deplyed in Tokyo Tech in March 2010. Furhtermore, virtual network technology will be useful in campus-wide network, so that we introduce such technologies which will be employed in Titanet3.

    CiNii Books

    J-GLOBAL

    researchmap

  • Design and deployment of campus-wide network using virtual network technologies

    TOMOISHI Masahiko, MASUI Kenji, IIDA Katsuyoshi

    IEICE technical report   109 ( 438 )   207 - 212   2010.2

     More details

    Language:Japanese   Publisher:The Institute of Electronics, Information and Communication Engineers  

    In campus-wide network, reliable and the state-of-the-art technology with low operational costs must be deployed. In this paper, we describe the design and deployment of the campus-wide network Titanet3, which will be deplyed in Tokyo Tech in March 2010. Furhtermore, virtual network technology will be useful in campus-wide network, so that we introduce such technologies which will be employed in Titanet3.

    CiNii Books

    researchmap

  • Interoperability Testing of NAREGI Grid Middleware for Large-Scale Cooperation

    HIGASHIDA Manabu, TOMOISHI Masahiko, SAKANE Eisaku, SATO Hitoshi, YAMANASHI Takeshi, OOBA Junichi, KOBAYASHI Taizo, MIZUTANI Fumiyasu, YAMADA Kiyoshi, TSUDA Tomoko, KONO Takahisa, AIDA Kento, MATSUOKA Satoshi, AOYAGI Mutsumi, SHIMOJO Shinji

    IPSJ SIG Notes   2008 ( 77 )   133 - 140   2008.7

     More details

    Language:Japanese   Publisher:Information Processing Society of Japan (IPSJ)  

    Four Information Technology Centers in Osaka University, Tokyo Institute of Technology, Kyushu University and Nagoya University deployed NAREGI Grid Middleware to their Supercomputing Resources under real operational scenarios, and tested its interoperability for nation-wide large-scale cooperation with two NAREGI R &amp; D centers: National Institute of Informatics and Institute for Molecular Science. We successfully demonstrated that we&#039;re able to formulate virtual organizations with certificates from multiple authorities and manage their grid resources, and also able to submit real grid applications to authorized computing resources with resource reservations, with coordinated execution across multiple meta-schedulers that issue reservation requests independently to potentially a same resource.

    CiNii Books

    researchmap

  • Interoperability Testing of NAREGI Grid Middleware for Large-Scale Cooperation

    東田学, 友石正彦, 坂根栄作, 佐藤仁, 山梨毅, 大庭淳一, 小林泰三, 水谷文保, 山田清志, 津田知子, 河野貴久, 合田憲人, 松岡聡, 青柳睦, 下條真司

    情報処理学会研究報告   2008 ( 77(OS-109) )   133 - 140   2008.7

     More details

    Language:Japanese   Publisher:Information Processing Society of Japan (IPSJ)  

    Four Information Technology Centers in Osaka University, Tokyo Institute of Technology, Kyushu University and Nagoya University deployed NAREGI Grid Middleware to their Supercomputing Resources under real operational scenarios, and tested its interoperability for nation-wide large-scale cooperation with two NAREGI R & D centers: National Institute of Informatics and Institute for Molecular Science. We successfully demonstrated that we're able to formulate virtual organizations with certificates from multiple authorities and manage their grid resources, and also able to submit real grid applications to authorized computing resources with resource reservations, with coordinated execution across multiple meta-schedulers that issue reservation requests independently to potentially a same resource.

    CiNii Books

    J-GLOBAL

    researchmap

  • Recent Topics of Wireless LAN Security Technology

    TOMOISHI Masahiko, YOSHIDA Shin-ichi, ITOH Toshiya

    IEICE technical report. Social Implications of Technology and Information Ethics   104 ( 96 )   1 - 6   2004.5

     More details

    Language:Japanese   Publisher:The Institute of Electronics, Information and Communication Engineers  

    The new IEEE standards of wireless LAN security and network technologies used in the standards are shown in this paper. The problem of WEP encryption discussed in the recent years are summarized, and TKIP technology and AES encryption for the next standard IEEE 802.11i are shown. For authentication, authorization, and accounting of wireless LAN client, IEEE 802.1X port-based network access control will be adopted in IEEE 802.11i. We explain EAP, RADIUS technologies, which gives the foundation for IEEE 802.1X. Finally, we show an example of management and operation of a wireless LAN environment using these technologies and point out some problems and prospects.

    CiNii Books

    researchmap

  • Secure implementation method of POP before SMTP using a relay server with SSL protocol

    K Masui, M Tomoishi, N Yonezaki

    ELECTRONICS AND COMMUNICATIONS IN JAPAN PART III-FUNDAMENTAL ELECTRONIC SCIENCE   87 ( 10 )   27 - 34   2004

     More details

    Language:English   Publisher:SCRIPTA TECHNICA-JOHN WILEY & SONS  

    POP before SMTP is a method of e-mail authentication in which users are authenticated by POP prior to SMTP connection. This method has been recognized by RFC2476, and is being increasingly employed. However, the danger of external attack is high if the POP server is operated in a demilitarized zone. In the implementation proposed in this study, POP server is protected by a firewall; for this purpose, POP connections to the gateway are relayed to an internal POP server, while the SMTP server remains in a demilitarized zone. In addition, security is improved by applying SSL to POP sessions between the relay server and clients. (C) 2004 Wiley Periodicals, Inc.

    DOI: 10.1002/ecjc.20105

    Web of Science

    Scopus

    researchmap

  • Secure Implementation Method of POP before SMTP Using a Relay Server

    MASUI Kenji, TOMOISHI Masahiko, YONEZAKI Naoki

    The Transactions of the Institute of Electronics,Information and Communication Engineers.   J86-DI ( 4 )   260 - 268   2003.4

     More details

    Language:Japanese   Publisher:一般社団法人電子情報通信学会  

    電子メールの送信時にユーザ認証を行うために,SMTP接続の前にPOPによるユーザ認証を要求する,POP before SMTPと呼ばれる方式がRFC2476において提案され,これを採用するサイトが増えている.しかし,POPサーバを非武装地帯で運用することは,外部からの攻撃を受けやすく危険性が高い.そこで,POPサーバをファイアウォールで保護するために,ゲートウェイヘのPOP接続をサイト内側のPOPサーバにリレーし,SMTPは従来どおり非武装地帯で運用する方法を提案する.更に,リレーサーバとクライアントの間のPOPセッションをSSL上で実行させることにより,セキュリティの向上を図る.

    CiNii Books

    researchmap

  • Secure Implementation Method of POP before SMTP Using a Relay Server with SSL Protocol

    MASUI Kenji, TOMOISHI Masahiko, YONEZAKI Naoki

    IEICE transactions on information and systems   86 ( 4 )   773 - 774   2003.4

     More details

    Language:English   Publisher:The Institute of Electronics, Information and Communication Engineers  

    POP before SMTP is a method for controlling access to SMTP servers. In this method, a user is required to be authenticated in a POP session before starting SMTP sessions. This method is very popular since the system is constructed on these basic protocols, however, when a POP server is located in DMZ, the server which might contain secret information such as mails has risk of being attacked by malicious users. On the other hand, an SMTP server should be located in DMZ, since an SMTP server is expected to have heavy traffic with other sites. In order to protect a POP server from attacks by means of a firewall, we introduce a new implementation method of POP before SMTP. In this implementation, a relay server which relays messages in a POP session to the POP server is located inside of the firewall. With the construction, the relay server monitors a POP session and notifies the result of the session to the SMTP server which is located in DMZ as in the case of usual setting. In addition, we improved security of the system by executing a POP session over an SSL channel.

    CiNii Books

    researchmap

  • リアクティブシステム仕様が段階的充足不能である原因 (第5回〔東京工業大学〕ネットワークシンポジウム講演論文集)

    友石 正彦

    NOC technical report   2 ( 1 )   1 - 4   2002.4

     More details

    Language:Japanese   Publisher:Network Operation Center,Tokyo Institute of Technology  

    CiNii Books

    researchmap

  • Report on FME 2001: Formal methods for increasing software productivity

    Masahiko Tomoishi

    Computer Software   18   455 - 460   2001.12

     More details

  • Design of unix system for the prevention of damage propagation by intrusion and its implementation based on 4 4BSD

    Kenji Masui, Masahiko Tomoishi, Naoki Yonezaki

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)   2200   536 - 552   2001.1

     More details

    © Springer-Verlag Berlin Heidelberg 2001. On usual UNIX systems, a privileged user of root is allowedto acquire any user’s authority without authentication process. If anintruder obtains the root privilege by taking advantage of system’s securityhole, he can abuse network reachability of any user of the system tobreak into other sites. Thus we present a new system design where theauthority of users is protected from root by introducing a new user substitutionmechanism. However, even if we introduce the new mechanism,on usual UNIX systems, the intruder can get the authority using manyother methods for root. We implement the new user substitution mechanismand the mechanisms which prevent the intruder from using suchmethods in FreeBSD-4.2, and confirm that the system design is effective.

    Scopus

    researchmap

  • Design of UNIX System for the Prevention of Damage Propagation by Intrusion and Implementation Based on 4.4BSD

    MASAHIKO TOMOISHI

    Information Security, LNCS   2200   536 - 552   2001

     More details

  • 合成可能なタブローによる仕様の差分的無矛盾性判定について (プログラム変換と記号・数式処理)

    友石 正彦, 米崎 直樹

    数理解析研究所講究録   1125   142 - 149   2000.1

     More details

    Language:Japanese   Publisher:京都大学  

    CiNii Books

    researchmap

  • リレーサーバを用いたpop before smtpのセキュアな実現法とその解析

    増井健司, 友石正彦, 米崎直樹

    日本ソフトウェア科学会第17回大会講演論文集   15 - 19   2000

     More details

  • Evolutional tableau method for temporal logic specifications

    M Tomoishi, N Yonezaki

    INTERNATIONAL SYMPOSIUM ON PRINCIPLES OF SOFTWARE EVOLUTION, PROCEEDINGS   2000-January   176 - 183   2000

     More details

    Language:English   Publisher:IEEE COMPUTER SOC  

    In this paper, we present a new consistency checking method for temporal logic specifications. The new method verifies consistency of a whole specification by using a tableau graph constructed from tableau graphs obtained on the verifications of partial specifications. The new method is applicable not only to on-the-fly verification, but also to comositional verification By on-the-fly verification, Ive mean a verification that proceeds as a specification is evolved. Compositional verification is verification constructed by merging modular verifications. By verifying a specification at each step of its refinement, we carl make specification evolution process efficient.
    A tableau graph constructed by a traditional tableau method does not suit reuse. The traditional tableau method has two phases; a tableau graph construction phase and eventuality checking phase. It is difficult to reflect the results of the eventuality checking on the tableau graph because there is no suitable substructure which can keep the results. For that reason, it is necessary to check eventuality formulae repeatedly on the reuse of the tableau graphs
    A tableau graph, introduced in this paper has a new structure and is obtained by piling up tableau graphs of subformulae, In this new structure, the checked results of eventuality checking are encoded. Therefore, all the results of the verification in each step can be reused for constructing the verification for a whole specifcation.

    DOI: 10.1109/ISPSE.2000.913236

    Web of Science

    Scopus

    researchmap

  • 段階的充足不能なリアクティブシステムの原因について

    日本ソフトウェア科学会第16回大会論文集   429 - 432   1999

     More details

  • 合成可能なタブロによる仕様の差分的無矛盾性判定について

    Program Translation, Symbolic Computation and Algebraic Manipulation(PSF99)   142 - 149   1999

     More details

  • Specifying the defective parts for modification of reactive system specifications

    Masahiko Tomoishi, Naoki Yonezaki

    International Workshop on the Principles of Software Evolution(IWPSE99)   1 - 7   1999

     More details

  • Finding the causes of un-realizability in temporal specifications

    Masahiko Tomoishi, Naoki Yonezaki

    International Workshop on Specification and Verification of Timed Systems (IWTS99)   0   1999

     More details

  • UNIXシステムにおけるroot権限の階層化

    増井健司, 友石正彦, 米崎直樹

    日本ソフトウェア科学会第16回大会論文集   45 - 48   1999

     More details

  • Detection method of Un-realizability Origins in Reactive System Specification

    NAKAMURA Masanobu, TOMOISHI Masahiko, YONEZAKI Naoki

    Technical report of IEICE. SS   97 ( 630 )   17 - 24   1998.3

     More details

    Language:Japanese   Publisher:The Institute of Electronics, Information and Communication Engineers  

    A reactive system maintains some interaction with its environment. It is necessary for its specification to be realizable that the specification has some special properties such as satisfiability, strong satisfiability and so on. When some specification doesn&#039;t have some of such properties, it is convenient to detect the specification&#039;s parts that break the property. Our purpose is to find the origins of un-realizability, to specify defective parts of an un-realizable specification. We first formalize causes of unsatisfiability in a specification, then introduce a method to derive all the causes at one try from a given specification.We also give a proof of the correctness of the method.

    CiNii Books

    researchmap

  • Consistency Checking on Composite Specification by Tableau Composition

    TOMOISHI Masahiko, YONEZAKI Naoki

    Technical report of IEICE. SS   97 ( 390 )   17 - 22   1997.11

     More details

    Language:Japanese   Publisher:The Institute of Electronics, Information and Communication Engineers  

    On the verification of a reactive system specification, it was not possible to reuse the verification by-products of its parts. We present a consistency checking method with news tableau graphs that can make it possible. The main idea of the tableau construction is based on the new way of representaton and examination f eventualities, where storongly connected parts are kept as a collection of symple loop structures.

    CiNii Books

    researchmap

  • Unification in Modal Logic with non-elementary frames

    友石 正彦, 萩原 茂樹, 米崎 直樹

    全国大会講演論文集   55 ( 0 )   559 - 560   1997.9

     More details

    Language:Japanese  

    本研究では, フレームのクラスが一階の制約で特徴づけられない体系KMに対して分解証明法を定義する。公理Mは時系列モデルが終了状態に到達することを表しており, デッドロックがないこと証明するのに利用することができる。このために, まず, 一階の制約でフレームが特徴づけられる体系に対する様相記号列の統一化による分解証明法を構成する。これまでも, Untilを持つ論理について公理系に基づいて規則を定義するものや, □に支配されるの選言肢, ◇に支配される連言肢を展開しない形の節形式を用いるものが提案されているが, 本研究では, 様相記号へのラベリングに対して意味論を記述する一階の言語におけるスコーレム化と対応をとることで, 節がラベルづけられた様相記号列をprefixとするリテラルの選言肢となる節形式を導入する。これにより, これまでに述語論理などの分解証明法において研究されてきた戦略を様相論理の分解証明法に導入する際の見通しがよくなるだけでなく, 証明の途中で選言, 連言を展開する必要がなく, 証明が分解規則によるステップのみとなるため証明の流れが見やすい。次に, 一階の言語におけるスコーレム化と対応できないKMの場合について分解証明法を拡張する。

    CiNii Books

    researchmap

  • Evolutional Tableau for Temporal Logic Specications

    Tomoishi Masahiko, Yonezaki Naoki

    IEICE technical report. Theoretical foundations of Computing   94 ( 181 )   37 - 46   1994.7

     More details

    Language:Japanese   Publisher:The Institute of Electronics, Information and Communication Engineers  

    logic with &quot;unless&quot; operator.This method is based on a tableau p roof system which reuses tableau graph in previous step.We suppose requirement specification description process is performed step by step.In this setting cheking specifications at each stage is more efficient than checking the total specifications once at the final stage,since we often specify contradicting requirements and to know contradicting part of specifications at an early stage helps us to get final consistent specifications.The problem of the stepwise chocking is that,if the checking process takes a time at each stage,then this approach becomes unrealistic.Our approach overcomes this problem by introducing the following ideas based on the new representation of tableau graphs and an introduction of new kind of canonical models.The main advantage of Obr new method is that it reuses tableau graphs generated for the specification at earlier stages.It avoids generating a subgraph which is the same as or similar to a graph generated previously.

    CiNii Books

    researchmap

▼display all

Presentations

  • 仮想ネットワーク技術を用いたキャンパスネットワークの設計と構築

    電子情報通信学会・技術研究報告  2010 

     More details

  • 無線LAN におけるセキュリティ技術の動向

    SITE2004-1  2008 

     More details

  • 送受信内容の相関を利用したhttpアクセス制御のためのプロキシ

    マルチメディア、分散、協調とモバイル(DICOMO2001)シンポジウム  2001 

     More details

  • 送受信メッセージのパターン解析によるhttpアクセス制御

    日本ソフトウェア科学会第18回大会  2001 

     More details

  • Design of unix system for the prevention of damage propagation by intrusion and its implementation based on 4.4BSD

    Information Security Conference 2001  2001 

     More details

  • リレーサーバを用いたpop before smtpのセキュアな実現法とその解析

    日本ソフトウェア科学会第17回大会講演論文集  2000 

     More details

  • UNIXシステムにおけるroot権限の階層化

    日本ソフトウェア科学会第16回大会論文集  1999 

     More details

  • 段階的充足不能なリアクティブシステムの原因について

    日本ソフトウェア科学会第16回大会論文集  1999 

     More details

  • 合成可能なタブロによる仕様の差分的無矛盾修正について

    プログラム変換と記号・数式処理  1999 

     More details

  • 有礎構造を意味論にもつ様相論理の分解証明法

    日本ソフトウェア科学会第15回大会論文集  1998 

     More details

  • パスワードクラック防止のためのunixのパスワードシステムの改善

    情報処理学会第62回全国大会論文集(CD-ROM)  2001 

     More details

  • 初等的でないフレームを持つ様相論理の統一化による証明法

    情報処理学会第55回全国大会講演論文集  1997 

     More details

▼display all

Research Projects

  • DNS不正情報汚染に対する効率的検知除去・再感染防止・端末除染の統合的設計と構築

    Grant number:18K11291  2018.4 - 2023.3

    日本学術振興会  科学研究費助成事業  基盤研究(C)

    友石 正彦, 金 勇

      More details

    Grant amount:\4290000 ( Direct Cost: \3300000 、 Indirect Cost:\990000 )

    本年度は4件、DNSを利用したセキュリティ、プライバシ実現の研究について成果発表を行った。
    DNSの実際の利用あたっては、組織単位でのキャッシュサーバの利用が一般的であるが、悪意情報を注入する「キャッシュポイズニング」攻撃が問題となっており、完全な解決には至ってない。代表的な対策としてDNSSECがあるが、端末汚染、乗っ取られた正規サーバからの攻撃への対策にはならない。そこで、それらも含めた、悪意情報注入を検知・削除、汚染元の端末特定が可能な機構の構築を目的とした研究を継続している。具体的には、キャッシュサーバにおいて名前解決履歴を取得し端末毎の履歴が検索可能なデータベースを構築、クライアントからのDNSトラフィックに対して正規データや過去データと統計的に比較することで異常を検知・削除する仕組みの構築を目指している。
    本年度は、キャッシュサーバ、履歴データベースを含むローカルネットワーク環境を構築し、提案手法によるプロトタイプシステムを構築、その機能評価を行った。また、それらによって国際会議にて発表を行った。
    また、スマートホーム等、家庭内に配置されるIoT機器から収集される情報をクラウドを通じて利用者のモバイルデバイス等でモニタするときに、プライバシを維持しつつ、大規模化する基盤についても研究を進めた。
    それ以外の関連の研究成果として、端末側DNS情報を用いた異常検知方法についてと、端末側DNS問合せにおいて複数のサーバを安全ポリシーを実現する方法について発表を行った。

    researchmap

  • Study of the autonomous path control method for the purpose of the effectiveness performance enhancement of the data transmission

    Grant number:22500054  2010.10 - 2013.3

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research  Grant-in-Aid for Scientific Research (C)

    TOMOISHI Masahiko, MASUI Kenji

      More details

    Grant amount:\3250000 ( Direct Cost: \2500000 、 Indirect Cost:\750000 )

    In the thing communication in everyday Internet life, communication may become slow though the communication channel is not congested in fact.
    In this study, we confirm it by reproducing that such a matter is really generated in our making experiment environment, find how to happen according to making it reappear by various cases, and are intended proposing how the whole communication performance rises by changing only a setup of the machines in a communication channel.

    researchmap

  • Verification methods of secure systems based on logical specifications

    Grant number:12133204  2000 - 2003

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research  Grant-in-Aid for Scientific Research on Priority Areas

    YONEZAKI Naoki, YOSHIURA Noriaki, NISHIZAKI Shin-ya, YONEDA Tomohiro, TOMOISHI Masahiko

      More details

    Grant amount:\40500000 ( Direct Cost: \40500000 )

    Our research results fall into fourfold.
    1)Verification and synthesis method for keeping safety of reactive systems. We developed verification methods for specifications of reactive systems. These verification systems examine whether a specification satisfy the condition that for any infinite behavior of environment, the reactive system can properly react against it forever. We found various techniques for the implementation of an efficient verification system.
    2) Network security. We defined an axiomatic system that can verify security properties of security protocols. Based on this inference rules, we also design construction rules for security protocols. By introducing several criteria of costs of protocols, optimized protocols are generated for each purpose. We also developed an analysis method for fairness of auction protocols. A new computational model is introduced, with which we can analyze the resistivity of the system for this kind of attack.
    3) Construction of secure system architecture. Once an intruder succeeds to get privilege of the super-user, he can easily intrude connecting other systems by abusing user switching mechanism. For this security problem, we gave a solution in which the user interfaces of other system components are unchanged but we introduced user authentication mechanism to the user switching mechanism. The intruder trying to avoid this mechanism is also detected in our system.
    4) Fundamental theories. We analyzed various encryption schemes and hash functions in axiomatic way and strictly formalized various security properties e.g. partial information of contents in cipher text cannot leak out. We also proved their sufficient conditions. Analysis of such security properties in axiomatic way is new and is not found anywhere. For verification of reactive systems, we gave a proof method for temporal logic of finite frames and prove its completeness. It is not trivial to give the complete proof method because finiteness is not first order definable.

    researchmap

  • 実現不能な仕様の欠陥情報を用いて部分プログラムを合成する方法に関する研究

    Grant number:12780194  2000 - 2001

    日本学術振興会  科学研究費助成事業  奨励研究(A)

    友石 正彦

      More details

    Grant amount:\1800000 ( Direct Cost: \1800000 )

    本年度は、実現不能な仕様の欠陥情報を用いて部分プログラムを合成するため欠陥情報の検出方式の形式化を行なった。また、その導出手続きの構成を行った。また、ネットワーク上で、いくつかのセキュリティシステムの構成を行った。
    1.仕様の段階的充足不能性の原因について考察し、その形式化を行った。また、その導出手続きを構成し、その手続きについて考察を行った。その結果、出力に関して決定化を行うだけでは、段階的充足不能の原因の健全な手続きを作ることができるが、それだけでは完全とはならないことがわかった。このため、段階的充足不能の原因を充足可能性を検査するタブローから計算するためには、新たな決定化のためのパラメータを付随して、計算する必要がある。
    2.HTTPの中継のためのリアクティブシステムの実装を実際に行なった。これは、ファイアーウォールを導入したネットワークにおいて、ユーザインタラクションのパターンに応じて中継の可否を切り替えるシステムである。
    ここで取り扱われる中継のための仕組み(状態繊維)単純なので、本研究での仕様と検証における実例として使いたいと考えている。
    3.いくつかのセキュリティのためのシステムを組込んだUNIX OSの拡張を行った。これは現UNIXのユーザ権限のデザイン、特にルート権限を見直すことによって、ネットワークを通じての成り済ましなどの可能性を減らす拡張である。
    ここで実装を行ったネットワークアクセスを行うまでの権限の委譲のシステムについても上記の検証システムによって実際に検証できればと考えている。

    researchmap

  • 計算機ネットワークの発展支援機構に関する研究

    Grant number:10139212  1998

    日本学術振興会  科学研究費助成事業  特定領域研究(A)

    今泉 貴史, 萩原 威志, 権藤 克彦, 友石 正彦, 鈴木 正人

      More details

    Grant amount:\2000000 ( Direct Cost: \2000000 )

    発展機構を備えたソフトウェアを構築する場合、プラットフォームとしてのネットワークが発展する点も考慮しなければならない。ネットワークの発展としては、新たなハードウェアの追加などが考えられるが、この場合にそのハードウェアを利用可能にするには管理者による設定が必要である。この管理の手間を省くために、アプリケーションの自動インストールに注目した。昨年度は、アプリケーションの設定をサイト内でどのように配布するのかについて研究を行った。今年度は、実際にアプリケーションをインストールする方法について研究を行った。
    今年度開発したシステムAPPCSは、インストールの際に行われるファイル書換やオプション指定などの情報を保存し、その情報をネットワーク内に配布することによりインストール作業を支援する。ユーザがネットワーク内のいずれか一台のホストでアプリケーションを手動でインストールすれば残りのプラットフォームに関してはそのホストで行われたファイル書換やオプション指定の情報を元に、APPCSがアプリケーションを自動でインストールする。
    APPCSはネットワークの全てのホストで常時動作しており、ユーザが行うインストール作業を監視しインストール手順の情報を集める。この情報を他のホストのAPPCSに送信し各ホストでこの情報を元に自動でアプリケーションをインストールする。このとき上位機のみ起動している時に上位機が仮インストールを行い、下位機が復帰した時に再度インストールする事でアプリケーションの可用性を高めるように設計した。
    我々はこのAPPCSを実装し、3種類の異なるプラットフォーム持つネットワーク環境において実験を行い、共有ディレクトリ毎にアプリケーションをインストールする方法と比べインストールの手間が省ける事及びアプリケーニションの可用性が高まる事を確認した。

    researchmap

  • Research on Specification and Verification of real-time software

    Grant number:07680341  1995 - 1997

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research  Grant-in-Aid for Scientific Research (C)

    YONEZAKI Naoki, TOMOISHI Masahiko

      More details

    Grant amount:\2300000 ( Direct Cost: \2300000 )

    It became crucial issue to build correct software with real time feature for safe critical systems e.g.embedded software in control systems. In order to make these software safer and securer, we need a new software construction method based on verification technique. In this research project we had the following results.
    1) Proof systems of temporal logic for various time domains
    First we developed connection calculus for temporal logic with discrete time domain. To prove the validity of a formula in discrete frames, we have to check the unsatisfiability for infinite frames. This means that we need substituion for infinite length of modal operators in connection calculus. In our approach we allows self substitution for modal operators so that we can solve the problem.
    Then next we studied axiomatic systems for a temporal logic with real number timed domain. We showed that it is neither possible to construct complete axiomatic system nor to give decision procedure for the validity of a formula. We restricted it to rational domain where the number of the charge of state is bounded, as a result we had decidable logic.
    2) Various aspects of software verification
    2-1) Differential verification method for temporal specification
    We developed new tableau method for differential verification, where the verification result for the previous specification is reused with the difference between a new specification and the previous one.
    2-2) Level of realizabilities of a specification and its decision procedure
    We defined several concepts approaching realizability. The classification of specifications based on these concepts gives us useful information for making a specification realizable. We gave the decision procedure for the membership of the classes and also we had an idea to identify a set of the parts of the specification which is the cause of un-realizability.

    researchmap

▼display all