2022年は戦争がはじまり、時代が逆行したような年でした。我々は技術者・研究者であるので、社会的・政治的には時代が逆行しても、科学と技術を進歩させ、科学技術で社会問題を解決してきたい所存であります。 『ゼロから学ぶRust』を執筆した 2022年12月13…

大学でセキュリティ関連の演習を行いました。この演習では、大学院生と社会人が研究や実装を通して実践的な学習を行います。トピックはRewrite it in Rust、モデル検査、ゼロトラスト、暗号など色々あるのですが、そのうちRewrite it in Rustのトピックを選…

RustでRaspberry Pi 4をどれだけ操作できるか興味があったので、連休期間にやってみました。制約は、Rustのasync/awaitを使うこと、rppalというembedded-halベースのライブラリを利用することです。結論から言うと、I2C、SPI、GPIOなどほとんどの操作はRust…

これは、Rust Advent Calendar 2021 (2)の25日目の記事です。 https://qiita.com/advent-calendar/2021/rust2021年8月にオライリー・ジャパンより出版された『並行プログラミング入門』を執筆しました。並行プログラミング入門 ―Rust、C、アセンブリによる実…

『知の限界』という本を買ったら第一不完全性定理をLispで実装する方法が載っていた。しかし、そのコードはSchemeでは動かないように思えたので、Schemeで実装をしてみた。不完全性定理では、コード中の引数に自身のコード渡して、自己言及的なゲーデル文Gを…

ざっくりというならば、モデル検査とは、仕様を（様相）論理式に落とし込んで、その仕様がモデルを満たしているかを検査するための方法論である。TLA+はモデル検査用のツールであり、仕様や実装の正しさを検証することができる。自分はモデル検査ツールはNuS…

Qumcumという学習用のロボットがあると知り合いに教えてもらったため、買ってみて遊んでみた。Qumcumはその知り合いが学生時代の時の教員だったらしい。Qumcumは自分で組み立てを行い、プログラミングして動かせるようなロボットである。組み立てはドライバ…

現在、BLispというプログラミング言語を設計・実装中で、基本機能は出来たので、とりあえずのドキュメントを作成して公開した。https://ytakano.github.io/blisp/index.ja.html https://github.com/ytakano/blispこれを公開したのが2021年2月21日頃だが、6月…

環境構築 実験用のOSはUbuntu 20.10、x86_64を想定します。まず、Rustの環境を整えます。Rustの環境はrustupで構築できるので簡単です。Rustには大きく分けてstableとnightlyがあるのですが、今回はnightlyを利用します。具体的には以下のようにコマンドを入…

BLispはRust言語で実装されたベアメタル環境で動作するシェル、API定義言語として現在研究・開発をすすめています。動機は2つあります。1つが、せっかく静的型付けで型安全なRust言語を使っているのだから、Rustと協調動作するスクリプト言語でも静的型付け…

このブログ記事は、Advent Calender 2020, Rust 3、23日目の記事となります。自分は現在大学で教員をしていまして、セキュリティ系の研究室に所属しています。現在はセキュリティの講義を担当しており、そこでRust言語を教えているため、その内容を紹介しよ…

タイムライン Rust言語で簡単なファームウェア、OS、言語処理系を作成したが、そのタイムラインはだいたい以下のようなものであった。もともとは、Rustでどの程度できるか検証するために始めた実装で、OSを作る予定ではなかったのだが、やっていくうちに面白…

先月、国内最大のセキュリティ研究会であるコンピュータセキュリティシンポジウム 2020（CSS 2020）が開催され、そこで、Rust言語を用いてファームウェア、OS、言語処理系を設計・実装した話を発表しました。本来、CSS 2020はリアルで開催されるはずでしたが…

最近、定理証明支援のCoqを入門している。というのは、以前の職場にいたときの職場でもCoqをやっている先輩がいて、今回の職場でも定理証明支援系を使っている同僚がいて、しかも最近自分はプログラミング言語実装をやっているためか、Coqや依存型について聞…

ytakano.hatenablog.com↑前回 前回はQEMUでビデオメモリへの描画まではできたが、実機で描画はできていなかった。その後色々と試行錯誤した結果、実機でもマンデルブロ集合を描画することに成功した。現状、Raspberry Pi 4でのベアメタルプログラミングの記…

ベアメタルプログラミングとはOSなどを利用せずに、直接ハードウェア上にプログラムを走らせるプログラミング手法である。要するにOSなどを自分で作る練習にもってこいなのである。また、Rust言語は型安全なプログラミングであるにも関わらず、メモリへの直…

ゴールドバッハ予想とは、2より大きい偶数は2つの素数の和で表せるという予想である。例えば、18 = 5 + 13 や、34 = 3 + 31 となる。 ゴールドバッハ予想が誤りであることを証明するには、その反例を示せば良い。というわけで、ゴールドバッハ予想の反例を求…

情報科学をやってきたのだから、死ぬまでに一度自作のプログラミング言語を作ろうと思ったのが2016年後半ぐらいである。プログラミング言語とオペレーティングシステムは情報科学を志した者は誰もが一度は目指す道である（たぶん）。 しかし、思い立ったは良…