이벤트-B를 이용한 블록체인 합의 메커니즘의 공식 검증

요약

본 연구는 Event-B 방법을 활용하여 블록체인 합의 메커니즘과 스마트 계약에 대한 공식 검증 프레임워크를 제시합니다. 이 접근법은 표현에서 추상화, 불변 기반 증명, 시간 모델 검사를 배포 전에 안전성, 생존성, 중복 지출 저항성에 대한 형식적 점검과 결합합니다.

초록

본 연구는 Event-B와 Rodin 플랫폼을 활용한 블록체인 합의 메커니즘과 스마트 계약 동작에 대한 공식적인 검증 프레임워크를 개발합니다. 이전의 접근법이 주로 시뮬레이션이나 사례 기반 고립 계약 검증에 의존하는 것과 달리, 이 작업은 유한 상태 기계(FSM) 추상화, 불변 기반 증명, 정제화 모델링, 시간 논리 검증을 통합하여 작업 증명(PoW), 지분 증명(PoS), 이중 지출 방지 메커니즘을 분석합니다. 솔리디티 스마트 계약은 FSM으로 추상화되어 이벤트-B 기계로 인코딩되어 상태 전이 및 안전 제약을 공식적으로 명시할 수 있습니다. 거래 유일성, 상태 일관성, 접근 제어 강제, 원장 불변 보존 등 안전 속성은 Rodin에서 자동으로 생성된 증명 의무를 통해 검증됩니다. 총 312건의 증명 의무가 생성되었으며, 이 중 287건(92%)은 자동으로 해제되었고, 25건은 인터랙티브로 증명되어 완전한 불변 보장을 달성했습니다. 라이브니스 속성은 Computation Tree Logic(CTL)에서 명시되었고, 모델 검사를 통해 검증되어 교착 상태 자유와 PoS 조건 하에서의 최종 검증자 선택을 확인했습니다. 이중 지출 방지는 상태 일관성 원장 모델링을 통해 공식적으로 시행되었으며, 모든 도달 가능한 상태에서 고유성 제약이 입증되었습니다. PoW와 PoS에 대한 프로토콜 수준의 합의 논리는 세 가지 추상화 수준에 걸쳐 정교화되어, 단계적 정제를 통해 블록 무결성과 검증자의 정확성을 보장했습니다. 결과는 기계 검사 증명이 시뮬레이션 기반 평가를 넘어 검증 가능한 정확성 보장을 제공하여, 블록체인 시스템에서 정확성 보증과 프로토콜 수준의 견고성을 강화하는 엄격하고 재현 가능한 검증 파이프라인을 구축함을 보여줍니다.

서론

블록체인 기술은 중앙화된 권위에 의존하지 않고 분산 기록 관리를 가능하게 하는 분산 원장 패러다임으로 발전했습니다. 참여 노드 간에 원장 상태를 복제하고 합의 메커니즘을 통해 합의를 이끌어내는 블록체인 시스템은 개방적이고 적대적인 환경에서 무결성, 투명성, 변조 저항성을 제공합니다. Yaga 등¹에 의해 설명된 바와 같이, 블록체인 아키텍처는 암호학적 원시 요소, 분산 합의 프로토콜, 피어 투 피어 통신을 결합하여 검증된 거래가 계산적으로 변경이 불가능하게 만듭니다. 작업 증명(PoW)과 지분증명(PoS)과 같은 핵심 합의 메커니즘은 검증자 선택, 블록 검증, 원장 동기화를 규제합니다. 또한, 스마트 계약은 미리 정의된 규칙을 자율적으로 실행하는 프로그래머블 로직을 내장하여 금융, 의료, 거버넌스 등 다양한 분야에서 분산형 애플리케이션을 가능하게 합니다. 블록체인 기술이 고부가가치 및 안전이 중요한 환경에 점점 더 많이 배치됨에 따라, 합의 메커니즘과 스마트 계약 동작의 정확성을 보장하는 것은 운영 신뢰성 유지에 필수적임이 되었습니다².

탈중앙화된 특성에도 불구하고, 블록체인 시스템은 논리적 및 프로토콜 수준의 취약점에 취약합니다. 원장 일관성 제약이 엄격히 적용되지 않을 때 이중 지출 공격이 발생할 수 있습니다. 합의 수준에서의 약점, 예를 들어 잘못된 검증자 선택 논리나 결함 있는 블록 검증 규칙, 그리고 재진입 및 부적절한 접근 제어 등 스마트 계약 취약점이 배포된 플랫폼에서 상당한 재정적 손실을 초래했습니다. 경험적 테스트 및 시뮬레이션 프레임워크가 PoW 및 PoS 프로토콜의 동작을 평가하는 데 널리 사용되지만, 이러한 접근법은 포괄적인 정확성 보장보다는 설명적인 관찰에만 기여합니다. 시뮬레이션 기반 검증은 모든 도달 가능한 상태에서 불변 보존을 증명하거나 모든 실행 경로에서 안전성과 생존성 특성을 보장할 수 없습니다. 이러한 한계는 관찰 분석을 넘어 블록체인 시스템에 대해 엄밀하게 추론할 수 있는 수학적으로 근거 있는 검증 기법의 필요성을 강조합니다.

형식적 방법론은 수리 논리를 통한 시스템 명세와 검증을 가능하게 하여 이러한 기초를 제공합니다 ^3,4. 이벤트-B는 이 패러다임을 단계적 정제를 통해 확장하여, 시스템을 불변량에 의해 제한되는 추상적 상태 기계로 표현하고, 전이가 가드된 이벤트⁵로 모델링됩니다. Rodin 플랫폼은 증명 의무를 자동으로 생성하고 이를 지원하여 기계 점검으로 불변 보존과 상태 일관성 검증을 가능하게^합니다. B-Method⁷과 Z⁸과 같은 고전적 명세 기법은 불변 기반 추론과 형식적 정제가 다양한 개발 단계에서 시스템의 정확성을 보장할 수 있음을 보여줍니다. 이 방법들은 9,10,11,12,13 배치 전에 정확성을 보장하기 위해 임무 중요 및 안전 중요 시스템에서 널리 적용되었습니다. UML-B와 그래픽 정제 프레임워크와 같은 추가 확장은 복잡한 산업 시스템에 대한 정제 기반 모델링의 확장성을 더욱 입증합니다^{14, 15, 16, 17, 18, 19}. 이러한 발전은 정제 기반 형식 모델링이 강력한 정확성 보장을 유지하면서 시스템 복잡도를 효과적으로 관리할 수 있음을 보여줍니다.

블록체인 시스템에 대해서도 형식적 검증 접근법이 탐구되었습니다. SMT 기반 계약 검증 기법은 Solidity 프로그램 내 주장을 자동으로 검사하며, 논리적 위반이 발생할 경우^반례를 생성할 수 있습니다. VERISOL과 같은 도구는 스마트 계약^{검증 2}를 위해 유한 상태 추상화를 사용하며, 정리 증명 접근법은 계약을 F*²¹과 같은 형식적 추론 프레임워크로 변환합니다. 또한, 이더리움 가상 머신의 의미론적 형식화는 실행 의미론과 취약^{점 탐지}에 대한 엄격한 추론을 가능하게 합니다. 마찬가지로, Coq와 같은 정리 증명 환경은 합의 관련 보안 속성과 거래적 올^바름을 분석하는 데 적용되었습니다. 이러한 접근법은 귀중한 통찰을 제공하지만, 종종 계약 수준의 올바르기나 합의 수준의 속성에 독립적으로 초점을 맞추는 경우가 많습니다. 시스템 수준의 원장 불변량, 합의 상태 전이, 스마트 계약 동작은 명세 계층과 검증 산물 간 추적성을 유지하는 통합 정제 기반 프레임워크 내에 거의 통합되지 않습니다. 더불어, 기존 접근법 중 다수는 여러 정제 수준에서의 체계적인 불변 보존보다는 취약점 탐지 또는 논리적 주장 검사를 강조합니다.

본 연구는 Solidity 스마트 계약의 유한 상태 기계(FSM) 추상화와 Event-B 정제 모델링 및 기계 검사 증명 의무 이행을 Rodin 플랫폼 내에서 통합한 통합 형식 검증 프레임워크를 제안함으로써 이 방법론적 공백을 해소합니다. 계약 검증과 합의 모델링을 별개의 문제로 다루는 대신, 제안된 프레임워크는 PoW와 PoS에 대한 프로토콜 수준의 상태 전환, 원장 무결성 제약, 거래 고유성 조건, 스마트 계약 상태 진화를 단일 구조화된 모델 내에서 공식적으로 명시합니다. 불변성 보존, 트랜잭션 유일성, 제어 상태 전이, 원장 일관성 등 안전성은 이벤트-B 불변량으로 표현되며 자동으로 생성된 증명 의무를 통해 검증됩니다. 시간적 및 실행 순서에 의존하는 속성은 계산 트리 논리를 사용하여 명시되며, 정적 불변량을 넘어선 정확성을 보장하기 위해 모델 검사를 통해 검증됩니다. 핵심 방법론적 기여는 추상화 계층 간 명시적 추적 가능성을 확립하는 데 있습니다: 견고성 함수는 FSM 전이로 추상화되고, FSM 전이들은 Event-B 이벤트로 인코딩되며, 불변량과 시간적 명세는 해제된 증명 의무 및 모델 검사 결과와 직접 연결됩니다. 이 구조화된 매핑은 각 정확성 주장이 기계에 의해 검증된 증거로 뒷받침되고, 증명 기반 보장과 시뮬레이션 기반 관찰을 명확히 구분합니다.

이 작업의 범위는 정밀함과 분석적 명확성을 보장하기 위해 의도적으로 제한되어 있습니다. 모델링은 합의 메커니즘에 대한 프로토콜 수준의 상태 전이, 원장 무결성 제약, 거래 고유성 속성, 스마트 계약 상태 동작에 중점을 둡니다. 메시지 전파 지연, 복잡한 적대 전략, 포크 해결 메커니즘, 상세한 이더리움 가상 머신 가스 의미론과 같은 네트워크 수준의 측면은 정의된 추상화 경계 밖에 있습니다. 이러한 모델링 가정을 명시적으로 정의함으로써, 이 프레임워크는 검증 주장이 공식적으로 검증된 증명 증거와 일치하도록 보장합니다. 이 논문의 나머지 부분에서는 추상화 방법론, 이벤트-B 모델링 및 정제 과정, 불변 및 시간적 검증 절차, 그리고 그 결과 검증 결과를 제시합니다. 블록체인 프로토콜과 스마트 계약 검증을 정제 기반 형식 모델링과 기계 검사 증명에 기반을 두어, 이 연구는 분산 원장 시스템에 대한 방법론적 엄밀성을 강화하고 배포 전 정확성 보증을 강화합니다.

프로토콜

연구 입력
이 연구에서는 두 개의 Solidity 스마트 계약이 검증 입력으로 사용되었습니다. 전자는 Simple DAO 스타일의 계약으로, 재진입 사례 연구로 사용되었습니다. 두 번째는 계약 수준의 이중 지출 제약을 테스트하기 위해 설계된 얇아진 원장/상태 전환 계약이었다. 원래의 Solidity 소스 코드는 이 프로토콜에서 정의된 추상화 및 검증 프로세스의 입력 자료로 사용되었습니다. 이러한 계약에 사용되는 일반적인 변환 과정은 그림 1에 나와 있으며, 검증 과정에서 Solidity 소스 코드가 FSM, Event-B, SMV 모델로 점진적으로 변환되는 과정을 보여줍니다.

경계 모델링
형식 모델링은 스마트 계약의 제어 흐름 논리, 즉 함수 진입 및 종료 동작, 내부 실행, 계약 수준 상태 전이 등에 중점을 둡니다. 함수 가시성(공개, 외부, 내부, 사설)과 재진입 분석과 관련된 콜 스택 동작이 함께 표현되었습니다. 추상적 전이 유형(호출, 전송, 전송)은 에테르 전송 작업으로 취급되었습니다.

계약 수준의 불변량은 거래 고유성을 보장하고 추상화 경계 내 이중 지출을 방지하기 위해 정의되었습니다. 검증 선택과 블록 무결성 요구사항을 표현하기 위해, 프로토콜-로직 추상화 계층은 작업 증명(Proof of Work)과 스테이크 증명(Proof of Stake) 모두의 프로토콜 수준 상태 전이 측면에서 정의되었습니다.

추상화 경계에는 메시지 전달 일정과 지연, 포크 해결, 네트워크 적대자의 비잔틴 전략 사용, 이더리움 가상 머신 의미론, 네트워크 노드가 제어하는 가스 의미론, 예외 전파, 비동기 실행, 복잡한 대체 동작, 네트워크 수준의 최종성 등 네트워크 계층 요소는 포함되지 않았습니다. 따라서 이중 지출 결정의 결과는 계약 수준의 불변량에만 적용되며, 최종 성에 대한 네트워크 수준의 합의를 구성하지 않는다.

도구 및 구성
로댕 플랫폼은 Event-B(버전 3.7.0) 모델을 모델링, 정제, 증명 의무 생성 및 해제하는 데 사용되었으며, 이를 통해 PP, ML, SMT, Atelier-B 증명기가 자동적이고 인터랙티브하게 증명을 해제할 수 있었습니다. nuXmv 버전 2.0.0은 생성된 SMV 모델에서 CTL 모델 점검을 위해 완전한 CTL 탐색 모드로 실행되었습니다.

모든 검증 실행은 Ubuntu 22.04 LTS, OpenJDK 11, Python 3.10.12를 사용하여 통제된 컴퓨팅 환경에서 수행되었습니다. Web3(7.6.0), NetworkX(3.4.2), Matplotlib(3.8.0), Graphviz(0.20.3), NumPy(1.26.4), Pandas(2.2.2)가 시뮬레이션 및 시각화 요소를 구현하는 데 사용되었습니다. 이 설계는 동일한 실행 조건에서 실행될 때 형식적 검증 및 시뮬레이션 결과를 재현할 수 있음을 보장했습니다.

변환 워크플로우
이 검증 과정은 네 단계로 나뉘었습니다. 솔리디티 계약은 처음에 유한 상태 기계(FSM-SC) 표현으로 변환되었습니다. FSM-SC 모델은 이후 Event-B로 인코딩되었으며, 명확히 명시된 불변량과 정제도가 명확히 명시되었습니다. FSM-SC 추상화는 nuXmv 내에서 SMV 모델로 변환되었습니다. 검증 결과는 증명 의무 이행 및 CTL 모델 검사에 관한 통계로 보고되었으며, 반례는 사례로 제공되었습니다.

FSM 구조
각 계약은 다음과 같이 정의된 유한 상태 기계로 추상화되었습니다:

여기:
S = 상태 집합
S₀ = 초기 상태
T = 전이 관계
V = 가시성 매핑
G = 가드 술어
A = 동작/상태 업데이트.

알고리즘 1: Solidity에서의 FSM 구성
입력: Solidity 소스 코드
출력: FSM-SC

1) Solidity 계약 추상 문법 트리를 파싱합니다.
2) 구성자 정의로부터 초기 상태 S₀를 생성한다.
3) 각 Solidity 함수 f에 대해 별도의 제어 상태 S_f을 생성하고 {publical, external, inalal, private} ∈ 가시성 V(f)를 기록합니다.
4) 함수 f 내의 각 문장에 대해, 상태 변수 업데이트에서 요구/주장 조건과 행동에서 가드 술어를 추출하여 전이 t를 도출합니다.
5) 전이 t를 T로 추가합니다.
6) 이더넷 전송 작업(호출, 전송, 전송), 내부 및 외부 호출, delegatecall, 자폭, tx.origin 사용, 조건부 분기, 루프 구성에 대한 명시적 전이 유형을 생성합니다.
7) FSM-SC 반환 = (S, S₀, T, V, G, A).

그리고 각 Solidity 함수는 서로 다른 FSM 제어 상태와 연관되어 있습니다. 취약점 이해를 위해, 외부 호출 후 균형 업데이트가 이어지는 취약성 관련 실행 흐름을 명시적으로 순서화된 전이로 추상화했습니다. 그림 2 는 SimpleDAO 스타일 계약의 FSM-SC 예시 다이어그램을 설명하며, 이 구성 단계에서 진입 상태, 외부 호출 전이, 상태 업데이트 시퀀스가 어떻게 추상화되었는지를 보여줍니다.

FSM을 이벤트-B로 인코딩하기
FSM 전환은 이벤트-B 구성체로 표현되었습니다. 모든 전이들은 특정 경비와 행동을 포함한 이벤트-B 이벤트에 대응합니다.

알고리즘 2: FSM에서 이벤트-B 인코딩
입력: FSM-SC
출력: Event-B 기계 및 컨텍스트

1) 계약 맥락에서 STATE_SET와 기능을 정의합니다.
2) FSM 제어 상태와 계약 수준 상태를 나타내는 변수를 선언합니다.
3) 각 FSM 제어 상태 s ∈ S를 current_state ∈ STATE_SET로 표현합니다.
4) 각 전이 (s → s′, g, a)에 대해, 다음과 같은 이벤트-B 이벤트 E_t을 생성한다:
5) 여기서 current_state = s ∧ g
6) 그러면 current_state := S′ ∥ 적용(a)
7) V(f)에서 파생된 가드를 사용하여 가시 제약 조건을 인코딩합니다.
8) 안전성과 일관성 특성을 포착하기 위해 inv1–inv9 불변량을 정의합니다.
9) S₀와 기본 값을 할당하여 초기화를 정의합니다.

상태 집합, 현재 상태, 함수 가시성, 호출 스택, 트랜잭션 타임스탬프, 이더넷 전송 상태, 위임자 호출 플래그, 자폭 플래그, 검증 조건 등이 이벤트-B 모델에서 포착되는 변수들입니다. 불변량(inv1-inv9)과 초기화 동작(act1-act6)은 형식적 명세의 동작과 일치한다. 그림 3 은 또한 취약점과 관련된 주요 이벤트, 특히 재진입 관련 전이가 Event-B 인코딩에서 어떻게 유지되는지 그래픽으로 보여줍니다. 이 그림은 그림 2에 표시된 FSM-SC 모델의 구조적 패턴이 검증 가능한 이벤트-B 이벤트로 어떻게 매핑되는지 설명합니다.

정제 전략
두 단계의 정교화가 구현되었습니다. 고수준 계약 제어 흐름과 코어 불변량은 추상 수준에서 표현되었습니다. 정제된 수준에서는 통화 스택 제한, 가시성 제한, 재진입 방지 조건 등 계약별 제한 사항이 추가되었습니다.

알고리즘 3: 정제화 및 증명-의무 해제
입력: 추상 기계 및 정제 기계
결과물: 탕감 증명 의무 및 통계

1) Rodin의 추상 기계에 대한 증명 의무를 생성한다.
2) 자동 프로버 실행 및 방전 결과를 기록.
3) 정제 기계에 대한 정제 증명 의무를 생성한다.
4) 정제 의무에 자동 증명기를 적용한다.
5) 필요 시 남은 의무를 인터랙티브하게 이행합니다.
6) 수출 증명 통계 및 상태 보고서.

증명 보고에는 불변량 수, 정제 수준, 생성된 증명 의무, 자동 방전률, 인터랙티브 방전율, 최종 방전율이 포함되었습니다.

CTL 속성 명세 및 모델 검사
FSM-SC 추상화는 nuXmv 분기 시간 검증을 위한 SMV 모델로 변환되었습니다.

알고리즘 4: FSM에서 SMV로, CTL 검사
출력: PASS/FAIL 검증 결과 및 반례 트레이스(있는 경우)

1. FSM 제어 상태를 열거된 SMV 변수 상태로 기록합니다.
2. FSM 전환을 가드된 next(state) 할당으로 변환합니다.
3. 외부 통화 및 잔액 업데이트와 같은 취약점 관련 조건에 대한 플래그를 유지합니다.
4. nuXmv에 CTL 속성을 인코딩하고 모델 검사를 수행합니다.
5. 속성이 실패하면, FSM 전이 시퀀스를 나타내는 반례 트레이스를 생성합니다.

CTL 검사에는 재진입 명령 요구사항, 전송 작업 후 상태 최종화, 중요 구간에 대한 무제한 재귀 진입 제한, 교착 상태 방지가 포함되었습니다.

보안 속성 검증
재입력을 방지하는 Simple DAO 스타일 계약은 외부 호출 간의 안전한 순서 조정과 상태 업데이트를 불변 및 CTL 제약을 통해 확인되었습니다. 허용되는 경우, 이 경비원들은 접근 제어 제약을 점검하여 무단 전이가 불변성으로 제한되도록 했습니다. 축소된 원장 모델은 계약 내 예방 수준에서 거래 고유성과 원장 일관성의 불변성을 검증했습니다.

보고된 산출물
결과 섹션은 FSM 구조 지표, 이벤트-B 모델 지표, 의무 증명 및 CTL 검증을 위한 통계 보고서를 제공합니다. 형식적 증명 결과와 CTL 모델 검사 결과를 별도로 제시하여 불변량에 의한 정확성 보장 증거와 시간 검증을 이용한 시간 검증의 증거를 구분합니다.

결과

이 연구의 결과는 Event-B와 CTL 모델 검사의 형식적 검증 산물과 블록체인 시뮬레이션에서 얻은 실행 가능한 정보를 결합합니다. 이러한 다층 출력의 결합은 스마트 계약의 핵심 동작, 합의 시스템, 그리고 설계의 제한된 예시 내에서 원장 건전성 한계를 검증할 수 있도록 지원합니다.

환경 설정 및 의존성 검증
모델 변환, 검증, 시뮬레이션에 사용된 실행 환경은 의존성 충돌 없이 실행되었습니다. Web3, NetworkX, Matplotlib, Graphviz, NumPy, Pandas를 사용하여 모든 암호학, 수학, 블록체인 상호작용 패키지가 로드되었습니다. 그림 4 에 표시된 콘솔 출력은 실행 시점에 필요한 모든 모듈이 식별되어 존재함을 나타냅니다. 이는 검증 및 시뮬레이션 활동을 수행하기 전에 계산 환경의 정확성을 검증하는 것...

토론

형식적 및 시뮬레이션 기반 검증은 해당 연구에 사용된 다층 검증 시스템이 잘 정의된 추상화 경계 하에서 스마트 계약 동작, 합의 메커니즘의 정확성, 원장-무결성 특성을 검증할 수 있음을 입증합니다. 이벤트-B는 안전성 특성, 상태 흐름, 재진입 방지 논리를 불변량과 정제 기반 논리 ^5,6 측면에서 수학적으로 근거 있게 표현합니다. 증명-방전 비율이 높다는 사실은 모델링되는 시스템이 내부적으로 논리적으로 건전하며, 9^{, 10, 11}, ¹²의 정확성을 입증하기 위한 공식 기법의 알려진 사용과 일치함을 의미합니다. PoS와 PoW의 시뮬레이션은...

재료

이 논문에 사용된 재료 목록

이름	회사	카탈로그 번호	댓글
로딘 플랫폼 (v3.7.0)	로댕 팀 / 이클립스 재단	https://www.event-b.org/install.html	이벤트-B 모델링, 정제, 증명-의무 생성 및 해제
이벤트-B 방법	사우샘프턴 대학교 / 로딘 커뮤니티	https://www.event-b.org/	불변 명세 및 정제를 위한 형식적 모델링 프레임워크
nuXmv Model Checker (v2.0.0)	FBK (브루노 케슬러 재단)	https://nuxmv.fbk.eu/	CTL 속성의 기호적 모델 검사
Graphviz (v0.20.3)	그래프비즈 팀	https://graphviz.org/	FSM 시각화 및 그래프 렌더링
Python (v3.10.12)	파이썬 소프트웨어 재단	https://www.python.org/downloads	시뮬레이션 및 실행 환경
Web3.py (v7.6.0)	이더리움 재단 / 기여자	https://web3py.readthedocs.io/	블록체인 상호작용 및 거래 시뮬레이션
NetworkX (v3.4.2)	NetworkX 개발자	https://networkx.org/	블록체인 및 FSM 구조의 그래프 모델링
Matplotlib (v3.8.0)	Matplotlib 개발 팀	https://matplotlib.org/	채굴 시간과 검증자 분포 도표
NumPy (v1.26.4)	넘피 개발자들	https://numpy.org/	수치 계산
판다스 (v2.2.2)	판다스 개발팀	https://pandas.pydata.org/	데이터 분석 및 처리
오픈JDK 11	오라클 / OpenJDK 커뮤니티	https://openjdk.org/projects/jdk/11/	Rodin 플랫폼의 필수 실행 시간
Ubuntu 22.04 LTS	캐노니컬 주식회사	https://ubuntu.com/download	모든 실험용 운영 체제
견고성	이더리움 재단	https://soliditylang.org/	입력으로 사용되는 스마트 계약 소스 언어
nuXmv 입력 언어 (SMV)	FBK	https://nuxmv.fbk.eu/documentation.html	CTL 검증을 위한 중간 모델 표현