Source-linked AI summary
Information Flow Control in Off-Chain Components
Stian Lybech, Eun-Young Kang, Riccardo Tonello, Anders Dalskov
TL;DR
Off-chain component는 smart contract를 on-chain 실행 범위 너머로 확장하지만, information-flow security를 형식적으로 검증하는 데 과제를 만든다. 이 논문은 concurrent formal model인 TinyChain을 개발하고, explicit loop가 없어도 recursive method call이 blocking behavior를 encode할 수 있으므로 standard static information-flow control이 실패함을 보인다.
문제
formal language semantics 없이는 smart-contract safety를 검증하기 어렵고, 특히 on-chain과 off-chain component를 결합한 architecture에서는 더욱 그렇다.
방법
이 논문은 concurrent한 on-chain 및 off-chain component, communication, broadcast synchronisation을 포착하는 formal smart-contract model인 TinyChain을 개발한다.
결과
off-chain component의 recursive method call이 explicit loop 없이도 blocking behavior를 encode할 수 있으므로, standard static information-flow control은 secrecy를 보존하는 데 실패한다.
시사점 및 한계
구현에 앞서 concurrent blockchain system의 security property를 연구하려면 Formal model이 필요하다. usual information-flow type system은 integrity와 secrecy를 직접 보장하지 않기 때문이다.
시사점 및 한계
recursive-call-based attack을 해결하려면 secret-value modification 또는 unbounded recursion을 금지해야 할 수 있으며, 어느 선택이든 significant restriction을 부과한다.
Abstract
from arXiv · showhide
This paper develops a model of a smart-contract language for a blockchain architecture with off-chain components. Off-chain components are pieces of smart contracts that execute at designated locations outside of the network of blockchain nodes, but remain synchronised with the on-chain contract state. They react to changes to the on-chain state, but may also notify the on-chain component about events in the world, e.g. stock prices, weather data etc., or even act as a bridge between different blockchains. This affords greater flexibility for the developer, but may also enable new vulnerabilities. As a concrete example, we use the model to study the problem of ensuring integrity and secrecy of data between the on-chain and off-chain components, using static information flow control techniques. This fails, even in the absence of a loop construct, because off-chain components act as separate threads and can encode a blocking construct e.g. through recursive method calls. We end the paper with a discussion of possible ways to remedy this situation.
1 서론
이 논문은 단일 언어를 넘어서는 blockchain 아키텍처를 포착하기 위해 inline off-chain components를 갖춘 형식적 smart-contract 언어 모델 TinyChain을 개발한다. 이 모델을 사용해 off-chain components가 recursive calls를 통해 blocking을 인코딩하므로 명시적 loop가 없어도 static information-flow control이 실패할 수 있음을 보인다.
- 동기: Off-chain components는 계산 비용이 큰 작업과 물리적 세계의 event와 지속적으로 상호작용하는 일을 blockchain 시스템에서 실현 가능하게 하지만, consensus control을 넘어서는 검증 과제를 도입한다.이들은 blockchain update에 반응하고, 외부 데이터에 접근하며, real-world system과 상호작용하는 동시에 consensus mechanism의 직접적인 통제 밖에서 데이터를 처리할 수 있다.
- 동기: 검증에서 Formal semantics가 중요한 이유는 사후적으로 정해진 semantics가 독립적인 specification이 아니라 implementation을 해당 언어의 실제 specification으로 남길 수 있기 때문이다.따라서 이 논문은 추상적 안전성 분석을 지원하는 작은 calculus를 정의한다.
- 형식 모델: TinyChain은 특정 smart-contract 언어 하나가 아니라 inline off-chain components를 갖춘 일반적인 blockchain 아키텍처를 모델링한다.이 calculus는 과 같은 접근법 및 TinySol 전통 을 따라 안전성 속성을 형식적으로 연구하기 위해 핵심 기능을 추상화한다.
- 형식 모델: 이 모델은 on-chain과 off-chain 실행 context 사이의 concurrency, point-to-point communication, broadcast synchronisation을 포착한다.그 semantics는 π-calculus 와 broadcasting systems 을 비롯한 communicating-system model을 기반으로 한다.
- Information-flow analysis: 이 논문은 Volpano, Irvine and Smith의 type system 을 포함한 static information-flow control 기법을 사용해 on-chain과 off-chain components 사이 정보 흐름의 integrity와 secrecy를 연구한다.이 적용은 hybrid architecture의 안전성 속성을 다룬다.
- Information-flow analysis: Static information-flow control은 명시적 loop가 없어도 실패한다. off-chain components가 별도의 thread로 동작하며 recursive method calls를 통해 blocking behavior를 인코딩하기 때문이다.이 결과는 그에 따른 verification problem에 대한 해결책 논의를 촉진한다.
2 아키텍처
아키텍처는 on-chain smart contract와 동기화된 off-chain component를 결합하며, 이 component는 계산 결과나 외부 세계의 이벤트를 다시 on-chain으로 전달할 수 있다. 트랜잭션은 on-chain에서 순차적으로 실행되고, 갱신된 상태는 off-chain node로 브로드캐스트되어 point-to-point 및 one-to-many 통신을 모두 가능하게 한다.
- 구성 요소: on-chain contract는 트랜잭션을 수신하고, 해당 off-chain component는 계산 결과나 외부 세계의 이벤트를 알리는 트랜잭션을 발행할 수 있다.
- 구성 요소: 사용자는 on-chain contract와 직접 상호작용하거나, 하나 이상의 off-chain node에서 실행될 수 있는 해당 off-chain component를 통해 간접적으로 상호작용한다.
- 통신: 상호작용은 두 node 사이 또는 사용자와 node 사이에서 point-to-point로 이루어지는 반면, 상태 갱신에는 blockchain에서 off-chain node로의 one-to-many 통신이 사용된다.
- 트랜잭션: contract는 서로를 직접 호출할 수 없다. cross-contract 호출은 현재 트랜잭션을 종료하고 새 트랜잭션을 예약하며, 등록된 callback을 통해 결과를 반환한다.
- 상태 동기화: 트랜잭션은 순차적으로 처리되며, 각 성공적인 완료는 갱신된 on-chain 상태를 모든 off-chain node에 게시한다.하나의 node는 여러 contract의 component를 실행할 수 있으며, 동일한 component가 여러 node에서 실행될 수도 있다.
3 언어 TinyChain
TinyChain은 local 및 remote method call, 명시적 fork, callback, 동기화된 on-chain/off-chain state를 지원하는 imperative Turing-complete smart-contract language다. 그 semantics는 parallel location, point-to-point transaction, broadcast, thread creation, 그리고 서로 구분되는 code·variable·read-only·writable-state environment를 모델링한다.
- 언어 구성: TinyChain은 표준 imperative statement와 별도 thread 실행을 위한 fork S1;S2를 결합하며, unbounded loop를 생략하더라도 recursive method가 Turing-complete 특성을 유지하게 한다.핵심에는 side-effect-free expression, local variable, this를 통한 contract-state access, assignment, sequencing, conditional이 포함된다.
- Method call: Remote call call d!e.f(e):eR은 지정된 location에서 method를 실행하고 callback list를 전달하며, local call은 out-parameter를 통해 결과를 반환할 수 있다.Callback 자체도 event list를 선언할 수 있어 contract와 location 사이의 event-driven interaction을 가능하게 한다.
- 실행 모델: 각 location은 parallel thread pool을 실행하며, off-chain component는 수정할 수 없는 read-only memory를 통해 broadcast blockchain update를 받는다.Network는 blockchain과 off-chain node로 구성되며, 각 location에는 writable shared memory, transaction, code environment도 존재한다.
- 통신 semantics: Operational semantics는 point-to-point transaction message d!T와 d?T를 broadcast state message X!envS와 X?envS 및 thread-creation action과 silent action으로부터 구분한다.Transaction에는 caller 및 callee identifier, method argument, callback event가 포함되며, caller는 sender로 이용할 수 있다.
- Semantic environment: Semantics는 contract code, local variable, contract 또는 off-chain state를 위한 environment를 사용하며, read-only envR memory와 writable envW memory를 분리한다.Local binding에는 this와 sender가 포함되고, envC는 method definition을 저장하며, state environment는 contract field를 value에 매핑한다.
4 정보 흐름 제어
이 논문은 TinyChain에 static information-flow control을 적용한다. TinyChain에서는 implicit 및 explicit concurrency로 인해 recursive blocking attack이 가능하며, loop가 없어도 secrecy가 무너진다. 기존 loop 기반 대응책은 적용할 수 없거나 지나치게 제한적이므로 bounded-recursion 기법이 필요하다.
- 4 정보 흐름 제어: TinyChain의 off-chain component는 별도의 thread로 실행되며, explicit fork concurrency는 blocking side channel을 통해 high-level 정보를 유출할 수 있다.이 공격은 concurrency와 shared state를 악용하며, Smith and Volpano 이 식별한 고전적 위협을 확장한다.
- 4 정보 흐름 제어: 재귀적으로 호출되는 block method는 transaction이 제공한 low value가 high secret과 같을 때만 진행함으로써 secret boolean을 유출한다.두 transaction이 off-chain execution을 유발한다. equality이면 진행과 assignment가 허용되지만, inequality이면 recursive blocking이 발생한다.
- 4 정보 흐름 제어: 이 공격은 integer로는 잘 일반화되지 않아 무한히 많은 추측이 필요하지만, bit-vector read를 사용하면 Smith and Volpano 에서처럼 bit-by-bit secret recovery가 가능하다.유한한 두 값의 boolean domain이 제시된 공격을 실행 가능하게 만든다.
- 4 정보 흐름 제어: 제안된 loop 대응책, 즉 loop guard와 body를 low security로 typing하는 방법은 recursive call에 직접 적용할 수 없으며, 그렇지 않으면 secret value의 수정을 금지하게 된다.recursive-call argument와 method body를 low-typed로 요구하는 것은 지나치게 제한적인 것으로 규정된다.
- 4 정보 흐름 제어: 향후 연구에서는 infinite recursion을 방지하면서도 secret value에 의존하지 않고 이를 수정하지 않는 unbounded recursion을 허용하기 위해 recursive call을 counting하는 방법을 제안한다.이 기법은 기존 loop 기반 해법과 결합할 수 있는 가능성이 있는 것으로 제시되지만, 실현 가능성은 아직 검토되지 않았다.
5 결론 및 향후 연구
이 논문은 off-chain component가 포함된 blockchain architecture를 위한 calculus인 TinyChain을 제시하며, transaction, thread, location, communication을 모델링한다. 또한 concurrent한 multi-component blockchain system에서 integrity와 secrecy에 초점을 맞춰 보안 추론을 위한 formal foundation을 제공한다.
- 결론: TinyChain은 transaction, thread, location, 그리고 location 간 communication을 사용해 off-chain component가 포함된 blockchain architecture를 모델링한다.이 모델은 Hyperledger Fabric 과 같은 multi-layer system을 포함해 여러 blockchain도 표현할 수 있다.
- 결론: 유사한 기존 연구 와 달리, 이 모델은 여러 component가 concurrent하게 실행되는 blockchain system에서 보안 속성을 추론할 수 있다.이 논문은 Additive Manufacturing 및 Cyber Resilience Act 와의 관련성 때문에 integrity와 secrecy에 초점을 맞춘다.